Closed9

パターンマッチの網羅性検査

解決策1:パターンマッチをコンパイルするとき、「すべてのパターンが失敗したらexit 1する」コードをパターンマッチの最後に追加する。
解決策2:コンパイル時にパターンの網羅性を検査する。

解決策2のほうが望ましそうなので、解決策2を目指す。そのためには、パターンの網羅性を検査する処理を実装しなければならない。そのための情報収集を行う。

元になった論文はこれらしい。

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という抽象を用いることで、複雑な型システムを持つ言語に対して、いい感じの網羅性検査を実現する

このスクラップは1ヶ月前にクローズされました
ログインするとコメントできます