パターンマッチの網羅性検査
星にゃーん前提：星にゃーんの自作言語Malgoは、パターンマッチを持つ。caseとかmatchとかのアレ。
問題：今の実装では、網羅的でないパターンを書くと、そのパターンマッチの動作が未定義（UB）
今の実装：https://github.com/malgo-lang/malgo/tree/815a6d2ca79a34eab6baf904403a43a3ccc0db5b
星にゃーん解決策１：パターンマッチをコンパイルするとき、「すべてのパターンが失敗したらexit 1する」コードをパターンマッチの最後に追加する。
解決策２：コンパイル時にパターンの網羅性を検査する。
解決策２のほうが望ましそうなので、解決策２を目指す。そのためには、パターンの網羅性を検査する処理を実装しなければならない。そのための情報収集を行う。
星にゃーん
「スペース」という概念を導入すると、網羅性検査が綺麗に書けるらしい。
星にゃーんSwiftでの網羅性検査の解説記事。スペースによる処理っぽい。
星にゃーん元になった論文はこれらしい。
Fengyun Liu. 2016. A generic algorithm for checking exhaustivity of pattern matching (short paper). In Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala (SCALA 2016). Association for Computing Machinery, New York, NY, USA, 61–64. DOI:https://doi.org/10.1145/2998392.2998401
星にゃーん読み始めた
星にゃーんADTに関する網羅性検査はsolved problemらしい。
MARANGET, L. (2007). Warnings for pattern matching. Journal of Functional Programming, 17(3), 387-421. doi:10.1017/S0956796807006223
星にゃーんしかし、型の継承、typecase、トレイト、GADTs、パス依存型（で定訳あってるっけ？）、合併型などなどの拡張を加えると、網羅性検査のアルゴリズムはメンテ不可能なほど複雑になる。
これを回避するためには良い抽象が必要。
星にゃーん"A generic algorithm for checking exhaustivity of pattern matching (short paper)."
では、spaceという抽象を用いることで、複雑な型システムを持つ言語に対して、いい感じの網羅性検査を実現する