Scattered clauses allowed after `end`?

[Timmmm]

I think it was recently noted that you don't actually need an end for scattered definitions, but I just discovered that you can have clauses after the end.

val foo : int -> int
scattered function foo

end foo

function clause foo(5) = 7

function main() -> unit = {
  print_endline(dec_str(foo(5)));
}

That prints 7. What exactly does end do? Seems almost like it's a nop?

[rmn30]

Originally I think scattered functions were effectively syntactic sugar for a function with all the clauses gathered together at the location of the end (conversely scattered unions were gathered at the original scattered declaration). This sort of works as it allows related union and function clauses to be placed together and intermixed. I'm not sure exactly how it works today. What happens if you move the call to foo before end foo? Also maybe having a separate val declaration makes a difference?

[Timmmm]

So... it still works almost completely backwards :-D

val foo : int -> int

function main() -> unit = { print_endline(dec_str(foo(5))); }

end foo

function clause foo(5) = 7

scattered function foo

I checked lots of possible orderings between the 5 lines. As far as I can tell the only ordering requirement is that val has to come before main. E.g. this works:

end foo

val foo : int -> int

function main() -> unit = { print_endline(dec_str(foo(5))); }

scattered function foo

function clause foo(5) = 7

Also maybe having a separate val declaration makes a difference?

I think this is required for scattered functions.

[rmn30]

Agreed, I think end is redundant and can even be omitted entirely. In terms of order I think the things that actually matter are:

• Function val declaration is before function call
• Function val declaration is before scattered function clauses
• scattered union U declaration is before any reference to union U e.g. function val declaration
• union clause X appears before any reference to X e.g. in a scattered function clause.

@Alasdair could confirm, and perhaps document?

[rmn30]

The scattered function declaration also appears to be unnecessary. If you include both a normal function definition and a scattered function clause for the same function you will get an error that it is already 'declared' (probably should say 'defined').

[Alasdair]

Right now the scattered function declaration and end for functions is very almost a no-op. You can omit both and just declare a function with val and then just define a bunch of separate clauses.

However for datatypes they could actually have some more usage, because we could use the end to tell future pattern-completeness checks that the scattered definition is now complete. The current pattern completeness checker doesn't really use this information, but I think it should.

We could allow:

scattered function foo : T

as I think this is allowed for mappings. We could also just change it to be:

scattered val foo : T

for both mappings and functions, and remove the separate scattered function and scattered mapping keywords, which might be a bit more consistent?