Enforce exhaustiveness checking for pattern match?

[Brandon Barker]

Is there a way to do this? I didn't find it at https://felix.readthedocs.io/en/latest/patterns.html (though maybe I misread something).

[John Skaller2]

> On 7 Dec 2018, at 01:03, Brandon Barker <brandon...@gmail.com> wrote:
>
> Is there a way to do this? I didn’t find it at https://felix.readthedocs.io/en/latest/patterns.html (though maybe I misread something).

There is an algorithm. Its very hard. It isn’t implemented.
And there’s a serious problem in Felix: pattern matches are desugared away long before type
checking.

In anticipation, I added special instructions that “record” the pattern match before it
was erased for this very purpose. But the algorithm is moderately difficult for
unguarded patterns and VERY difficult if there are guards.

I think the algo is due to Simon Peyton Jones but I’m not sure.
Ocaml implements it. But Felixi pattern matches are considerably
more powerful than Ocamls.

So I’d probably aim for partial checking, i.e. check certain cases,
such as if the top level is a variant, and all the arguments are
irrefutable (eg variables). Not general but will catch many cases.

The problem is SOME cases are deliberately incomplete.
The key difficulty is

let Some x = y in ….

There’s no way to check the None case because the syntax won’t allow it.
Its written the way it is *deliberately* because its asserting the None case
cannot occur in this context.

This is common in C, derefing a pointer: it means you KNOW the pointer
cannot be NULL.


—
John Skaller
ska...@internode.on.net