Gleam: Exhaustiveness checking of assignments and case expressions

[lpil]

Neelakantan R. Krishnaswami: Focusing on Pattern Matching

https://www.cl.cam.ac.uk/~nk480/pattern-popl09.pdf

P. Sestoft: ML pattern match compilation and partial evaluation

No link :(

Luc Maranget: Warnings for pattern matching

http://moscova.inria.fr/~maranget/papers/warn/warn.pdf
Was used by Elm.

Lennart Augustsson: Compiling pattern matching

https://link.springer.com/chapter/10.1007/3-540-15975-4_48

Possibly more than we want, we are interested in exhaustiveness checking alone now, no need for compilation as the Erlang VM will do this for us.

[lpil]

I was lucky enough to see Simon Peyton Jones talk about how this is now implemented in the Haskell compiler at Code Mesh LDN 2019 (talk title: REVISITING PATTERN MATCH OVERLAP CHECKS IN HASKELL).

The approach sounded good (and SPJ recommended that I use it when I asked) but the paper has not been released yet. Either work off the slides or see if the paper is out when we get around to implementing this.

I believe the same talk was given (possibly in more detail) at the Haskell eXchange 2019.

[OvermindDL1]

Can also see the OCaml compilers code for it, it's quite clean. :-)

[michallepicki]

Here is P. Sestoft: ML pattern match compilation and partial evaluation: http://dotat.at/tmp/match.pdf

[michallepicki]

Paper mentioned in SPJ's talk: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf

[michallepicki]

SPJ's talk got published: https://www.youtube.com/watch?v=SWO5OzSxD6Y

[CrowdHailer]

From the list of papers I guess this is not a good issue to start with.
Is there anything I can help with. is the SPJ approach the one that is accepted as the "right" approach for this issue?

[CrowdHailer]

From the list of papers I guess this is not a good issue to start with.
Is there anything I can help with. is the SPJ approach the one that is accepted as the "right" approach for this issue?

[lpil]

is the SPJ approach the one that is accepted as the "right" approach for this issue?

I didn't know how to evalute the options so I cornered SPJ at a conference and he told me I should use that one. Good enough for me!

[QuinnWilton]

I've been reading the SPJ paper tonight, and I think there's a few simplifications that apply to Gleam.

1) Since Gleam is strict, we don't need to worry about handling divergent sets or strictness constraints at all (I'm not positive on this and need to do a deeper pass to be sure)
2) Since Gleam doesn't support GADTs, we don't need to track type equalities (in rules CCONVAR and UCONVAR, see 4.3)
3) The satisfiability oracle can ignore all constraints and the algorithm remain sound (section 6.1)

By ignoring (3) to start, we lose exhaustiveness checking of guards, but it becomes possible to add support later without changing the core algorithm. This lets us avoid also having to write a type-constraint solver for the initial version. We could even leave out the CGUARD and UGUARD rules entirely to start, and add those later.

[QuinnWilton]

Also of note, the paper Elm used (Maranget) is mentioned under Related Work:

It sounds similar to SPJ's algorithm, but without support for GADTs, laziness, guards, or nested patterns. I'm no expert on this stuff, but SPJ's algorithm sounds like a natural evolution of things, even if only some of the new features are relevant to Gleam.

[lpil]

Amazing work!

RE GADTs: I would be interested in possibly having them at a later date so if we can be open to that extension then that would be excellent.

[QuinnWilton]

I think that it would just be a case of whether we track the type equalities in those two rules or not. I'm on my phone now and headed to sleep in a moment, so I can't grab a picture, but figure 2 (maybe it was 3) summarizes the algorithm, and as far as I could tell, support for GADTs comes from calculating Δ' in CCONVAR and UCONVAR.

Assuming we represented the type constraints as an enum, it'd just be a case of adding type equalities to that enum + tracking them there later.

I think the broad algorithm can be kept intact, and we just not track the things we don't care about yet.

I'm also not an expert on this stuff, so it'd be really helpful to double check with someone who is to make sure I'm not completely misunderstanding the algorithm :)

[QuinnWilton]

I've been doing a lot of research on this the past few days, and the 2015 GADT paper is considered by SPJ to be slow, brittle, and hard to understand.

His Code Mesh LDN talk describes a simpler approach at a high level (and is an excellent and very approachable talk).

I haven't read it in its entirety yet, but that talk seems to be formalized in a draft paper from March 2020, "Lower Your Guards": https://www.microsoft.com/en-us/research/publication/lower-your-guards-a-compositional-pattern-match-coverage-checker/

I'm not promising anything concrete yet, but I'm going to take a stab at implementing a reduced subset of this paper against a simple language in Elixir, to test its applicability to Gleam.

[lpil]

Amazing investigative work @QuinnWilton ! Thank you!