Coverage checking for case expressions and function definitions

[byorgey]

Either in a case expression or in a function defined by multiple pattern-matching clauses, it would be nice to have a checker that tests whether all the possible cases have been covered, and issues a warning if not. This is non-trivial, but well-studied.

[byorgey]

For example, https://www.microsoft.com/en-us/research/publication/lower-your-guards-a-compositional-pattern-match-coverage-checker/ is recent work in this area, and seems nice. We might be able to easily borrow their approach.

[byorgey]

Note, however, that arithmetic patterns complicate the story here quite a bit! However, my intuition tells me that it should be doable (with some very interesting math). For example, arithmetic patterns are constrained to be linear functions of their bound variable, and it should be tractable to check whether a collection of linear Diophantine functions covers all of N or Z, using the Chinese Remainder Theorem.

[byorgey]

I have upped the importance of this feature. After teaching about functions and emphasizing how functions have to be defined on all inputs, it is strange to then have Disco allow partial functions. We might even go so far as to require totality---though perhaps only up to nontermination. e.g. we would catch f(true) = 5 as being partial, but not f(x) = 1 + f(not(x)).

[byorgey]

Could be a nice research project for a student. I think as a first cut we should just focus on coverage checking, not termination. Termination checking could be something we tackle separately later.

[byorgey]

Some potentially relevant reference material: https://gitlab.com/yorickpeterse/pattern-matching-in-rust/-/tree/main/jacobs2021