Exhaustivity checks in pattern matching

[Aleksander Boruch-Gruszecki]

Hello,

I'm interested in how one would approch checking pattern matching for exhaustiveness - it seems like a very interesting problem. I already know of bondi and Pattern Calculus (at least that they exist). What other theory would I need to better understand the problem? Was this already solved for other languages (I'm assuming yes) and how much are those results related to the Dotty?

Thanks in advance,
Aleksander Boruch-Gruszecki

[Guillaume Martres]

If you haven't already, have a look at the proposed implementation in Dotty by
Fengyun and the links to reference at the end of his comment:
https://github.com/lampepfl/dotty/pull/1261#issuecomment-221736473

[Aleksander Boruch-Gruszecki]

Huh, I was under the impression that since the pattern matching is labeled as "under consideration" in the github readme, there's no implementation yet proposed. Will do, thanks!