30 Mar
2021
30 Mar
'21
10:53 p.m.
On 3/28/21 9:17 PM, Richard Eisenberg wrote:
I think this is the key part of Alexis's plea: that the type checker take into account exhaustivity in choosing how to proceed.
[…]
Does this match your understanding?
Yes, precisely. :) Without GADTs, exhaustivity doesn’t yield any useful information to the typechecker, but with them, it can. I agree with Simon that it seems tricky—his examples are good ones—and I agree with Richard that I don’t know if this is actually a good or fruitful idea. I’m certainly not demanding anyone else produce a solution! But I was curious if anyone had explored this before, and it sounds like perhaps the answer is “no.” Fair enough! I still appreciate the discussion. Alexis