Warnings for pattern matching

以下のようなパターンを弾く。

code:non_exhaustive.ml

(* (None, Some _) に対応するパターンがない: non exhaustive *)

let f = function

| (Some _, _) -> 0

| (None, None) -> 1

code:useless.ml

(* Some (Some _) は先に Some _ にマッチするため決してマッチしない: useless *)

let a = function

| Some _ -> 2

| None -> 1

| Some (Some _) -> 0

この論文では、ネストした構造を持つパターンを "平らな" 行列に変換していく。行がmatch式の一つのパターンに対応し、役立たずか判定する関数$ U はこれまでのパターンを表現する行列$ P に対して新たに加えるパターンを表現する行$ \vec{q} が役に立つかという形$ U(P, \vec{q}) で表現される。計算中、$ P は$ \vec{q} に応じてコンストラクタが展開されたり、関係のない行が取り除かれることでサイズが変化する。$ U を少し拡張して網羅できていないパターンを抽出する関数$ I も定義できる。

ここまではわりと率直なコードでおおよそのケースをカバーしているものの、Useless checkerについてはOr-patternが入るとまた少し話がややこしくなる。

code:useless2.ml

(* 2つめのパターンは全体としてはUsefulだが One _ や Cons (_, _) の部分はUseless *)

let f = function

| One x | Cons (x, _) -> x = 1

| Nil | One _ | Cons (_, _) -> false

ではどうすれば良いかというと、単に Or-pattern を展開する:

$ U(P, ((t_1|t_2), q_2 \cdots q_n)) = U(P, (t_1, q_2 \cdots q_n)) \; or \; U(P @ (t_1, q_2 \cdots q_n), (t_2, q_2 \cdots q_n))

実装上は、Or-patternとそれ以外を区別するために区切り $ \bullet を入れた行列$ P \bullet Q \bullet R およびベクトル$ \vec{p} \bullet \vec{q} \bullet \vec{r} が導入されている。式は非常に複雑だけどもやっていること自体は素直で、

1. ネストしたパターンを展開しつつ、$ Q に共通のパターンを、$ R にOr-patternを集める

2. 集め終わり、$ R が空ならば単純に$ U(Q, \vec{q}) でよく、そうでない場合は

3. ある列$ j \; (1 \leq j \leq z) , ($ z は$ R の列数) を選ぶ

4. その列$ j を検査対象として、$ R の他の列は共通のパターンとして考える

$ 2^z 通りの全てのパターンを生成する必要はない

5. 全ての列についてのuselessなpatternを合成して全体の結果とする