プログラミング言語: パターンマッチの意味解析

プログラミング言語のパターンマッチにおける意味解析の論文やアルゴリズムをつまみ食い

• 論文 Warnings for pattern matching
  • もっとも興味があるのは usefulness を判定するアルゴリズムなので、そこと前半の定義を中心に。
  • 遅延評価とかは無視
• これを基に実装されている Rust Analyzer のコード
• そのうち A Generic Algorithm for Checking Exhaustivity of Pattern Matching (スライド)

Introduction

パターンマッチングは ML 系プログラミング言語の重要な機能のひとつです。

パターンマッチングは、場合分けによる推論（およびプログラミング）に適しています。このような推論スタイルでは、ふたつの基本的なチェックが必要です。すべてのケースが考慮されているか？　そして、どのケースも他のケースに包含されているか？

これは、パターンマッチングの用語を使うと「すべての節 clauses が有用である網羅的なパターンマッチング式を書きたい」ということです。ML のコンパイラは、通常、これらふたつの基本的な要求を満たさないパターンマッチング式を異常 anomalies とみなして、警告やエラーを報告すべきです。そうすることで、コンパイラはプログラマがプログラム中のエラーを発見するための助けとなります。

パターンマッチングをコンパイルする方法は、決定木を対象とするか、バックトラック・オートマトンを対象とするかによって、ふたつのクラスに分類されます。両者を診断能力の点で比較すると、決定木の手法は、決定木が完全であり、不要なコードを含まないため、決定木に対してチェックを行うことができるという利点があります。これに対して、バックトラック・オートマトンは簡単には解析できません。

しかし、この論文の範囲を超えた理由 ^[1] により，一部のコンパイラ設計者はバックトラック・オートマトンを選択しています。たとえば、Objective Caml ^[2] の場合がそうであり、私たちの最初の動機は、このコンパイラのパターンマッチングのアルゴリズムを抽出することでした。つまり、最初のアイデアは、パターンマッチングの決定木へのコンパイルの簡易版を使用することでした。

しかし、パターンマッチングのチェックは、パターンマッチングのコンパイルよりもはるかに少ない労力で済むことが分かりました。最終的に得られたアルゴリズムは、ただ単に決定木へのコンパイルを簡略化した以上のものになりました。さらに、チェックに関する研究により、非常に一般的な解を得ることができました。私たちのアナライザは，意味論がまったく異なる ML と Haskell 両方に対して有効な答えを与えることができます。

本研究はふたつのパートに分かれています。第 1 部では、パターンマッチングのふたつの異常 anomalies を定義し、両方の異常を検出するアルゴリズムを紹介し、正格評価、遅延評価、および Haskell のセマンティクスに関して、このアルゴリズムの正しさを証明します。

第 2 部では、我々のアルゴリズムの実装について説明します。つまり、ユーザーに正確な警告を提供するという初期の実用的な問題に対して、我々のアルゴリズムをどのように改良し、適応させるかを示します。より具体的には、セクション 5 では、マッチしない値の例を提供することで、非網羅性の診断をより分かりやすくする方法を示します。次に、セクション 6 では、無効なケースの検出の重要な改良である無効なパターンの検出を検討します。この改良は、同じアクションを持つ節をグループ化する便利な機能である or-pattern を実装するときに自然に現れます。

最後に、我々の実装の効率性を分析し、結論を述べます。

第 1 部 異常検知のアルゴリズム

2. パターン、値、その他

ML の値のほとんどは、いくつかのシグネチャ上の基底項として定義できます。シグネチャは，データ型 data type の定義によって導入されます．例えば、以下のコード ^[1] では、

type mylist = Nil | One of int | Cons of int * mylist

型 mylist の値は、以下の 3 つのコンストラクタ constructor で構成されています。

1. Nil (0 引数のコンストラクタ = 定数コンストラクタ)
2. One (1 引数)
3. Cons (2 引数)

ML の値のほとんどはこのように定義されます。真偽値はふたつの定数コンストラクタをもつ型であり、整数型は無限個（または 2^{31} 個）の定数コンストラクタを持つと定義され、ペアは唯一の二項コンストラクタを持つ型 (中置演算子 "," で記述）などです。

より一般的には、値はいくつかのコンストラクタ上の（基底）項として定義されます。次のように明示的に定義しましょう。

以降では、定数コンストラクタの () は省略し、Objective Caml の文法に合わせます (NIl, true, 0, など)。^[2]

このシンプルな定義は、値呼び出し call-by-value の ML 言語におけるパターンマッチングの異常検知を研究する目的では十分です。しかし、

• 遅延評価の言語におけるパターン・マッチングの適切なセマンティクスは、部分的な値を定義する必要があり、これはセクション 4 で行います。
• 整数や文字列をはじめとする多くの値は、既知のシグネチャ（おそらく無限の大きさ）の上に構築された項と見なすことができますが、すべての値がそのように見なすことができるわけではありません。例えば、パラメトリックな多相性を示す型の関数や値を考えてみましょう。しかし、我々は、ML のすべての型や値の正確な性質には興味がありません。その代わりに、次のような非公式な公理に頼ることにします。任意の型 t が与えられたとき、t を型として持つ少なくともひとつの値が存在する、と仮定します。

厳密に言えば、この公理は成り立ちません。少なくとも、OCaml では値をもたない型を定義することができます。

type t_empty

そして、この型を使って、以下のようなヴァリアントをもつデータ型を定義し、それをパターンマッチに使うことができます。

type t = C of t_empty
let f x = match x with C y -> y

もちろん、上記の C y -> y は無効 useless なはずです。パターン C y にマッチする値は存在しません。しかし、前述の通り、今回のアルゴリズムでは t_empty に少なくともひとつの値が存在すると仮定しているため、これを無効とはみなしません。

同様の理由で、以下の例を網羅的ではない non-exhaustive と判定します。

type tt = A | B of t_empty
let g x = match x with A -> true

すでにお分かりの通り、この判定は間違っています。

t_empty 型の v をもつ B(v) という値は存在しないので、上記のパターンマッチは A -> true 節だけで、型 tt のありうる値すべてを網羅しているはずです。しかし、ほとんどの型に対して少なくともひとつの値が存在する公理が成立することを考えると、この問題は些細なことだと言えます。

パターンは値を識別するために使用されます。より正確には、パターンは共通の接頭辞を持つ値の集合を記述します。つまり、パターンは変数を持つ項であり、与えられたパターン p はそのインスタンス σ(p) (σ は置換の範囲) を記述します。しかし、ここではプログラミングに近い形で、パターンを以下のように定義したいと思います。

実際には、パターンの定義に変数は登場しません。変数はワイルドカード \_ で置き換えることができます。ワイルドカードは、名前を持たない変数と考えることもできます。また、ここでは、最近の ML 言語の実装で提供されている or-pattern を採用しています。

さらに、パターンが型付けされていることも重要です。つまり、パターンは、データ型の宣言によって強制されるルールに従っていることを前提にできます。Objective Caml のコンパイラは、型付けのあとにパターンマッチング解析を行うので、パターンは型アノテーションを持っています。以降では説明を簡単にするために、これらのアノテーションをすべて明示することは避けています。しかし、適切な場合には、型アノテーションを (p : t) として示すことがあります。

通常の項の理論では、t 型の項 v は、同様に t 型であるパターン p が項 v の接頭辞を記述している場合、v は p のインスタンスであると言います。つまり、σ(p) = v となるような置換 σ が存在するときです。線形パターンの場合、どんな変数も与えられたパターンに 2 回以上現れることはないので、インスタンス関係は帰納的に定義することができ、変数名は無関係です。

定義 1 (インスタンス関係)

任意のパターン p と、p と共通の型をもつ値 v が与えられた場合、インスタンス関係 p \preceq v は以下のように定義されます。

ここでパターンと値は型付けされていることを改めて強調しておきます。

特に \_ \preceq v はどんな値でも成立するわけではなく、指定された型 t の値 v に対してのみ成立します。さらに「型は空ではない」という公理の結果として、どのパターン p にも少なくともひとつのインスタンスが存在します。

上記の定義 1 では、\vec{p} = (p_1 \cdots p_a) , \vec{v} = (v_1 \cdots v_a) という便利な表記を使いました。\vec{p} と \vec{v} は、それぞれパターンと値の (行) ベクトルを表しています。

さて、ベクトルのインスタンス関係を定義しました。次に、パターン P = (p_j^i) は、m \times n の大きさの行列で、m は P の高さ (行数)、n は P の幅 (列数) を表します。行のない行列 (m = 0 かつ n \geq 0) は \emptyset と書き、空行のみの行列 (m > 0 かつ n = 0) は () と書きます。最後に、行列 P の行番号 i を \vec{p^i} と表記することがあります。

以降では、行列とベクトルという便利な枠組みの中で，ML のパターンマッチングの定義を思い出してみましょう。

• パターンと値は型をもつ
• すべての型は必ず値をもつ（公理）

ベクトルと行列の記法

定義 2. ML 言語のパターンマッチング

P をパターンの行列、\vec{v} = (v_1 \cdots v_n) を値ベクトルとします（n は P の幅に等しい）。P の i 番目のパターンが \vec{v} をフィルタリングするのは、次のふたつの条件が成立する場合に限られます。^[1]

1. (p_1^i...p_n^i) \preceq (v_1...v_n)
2. \forall j \lt i, (p_1^j...p_n^j) \npreceq (v_1...v_n)

また、このとき「\vec{v} がP の i 番目のパターンにマッチする」と言うことにします。

つまり，ベクトル \vec{v} は，行列 P の先頭から順に試行し、自分がインスタンスとなる最初の行にマッチします。ここでも、型付けされていることが暗黙の了解で、P のすべての行と \vec{v} は共通の型でなければなりません。

定義 2. 例1

型 mylist である 5 \times 2 の行列 P を考えてみましょう。

実際に、いくつかのベクトルがどのようにマッチするか試してみます。

1. ベクトル \vec{v} = (\mathtt{Nil}, \mathtt{Nil}) は P の最初の行にマッチします。なぜなら (\mathtt{Nil}, \mathtt{\_}) \preceq (\mathtt{Nil}, \mathtt{Nil}) (p_1^1 = \mathtt{Nil} \preceq \mathtt{Nil} = v_1) かつ p_2^1 = \mathtt{\_} = v_2 であるからです。
2. ベクトル \vec{w} = (\mathtt{One(0)}, \mathtt{Nil}) は P の 2 番目の行にマッチします。
   • (\mathtt{\_}, \mathtt{Nil}) \preceq (\mathtt{One(0)}, \mathtt{Nil}) ここから、\vec{w} は行列 P の 2 番目の行のインスタンスです。
   • (\mathtt{Nil}, \mathtt{\_}) \npreceq (\mathtt{One(0)}, \mathtt{Nil}) (p_1^1 = \mathtt{Nil} \npreceq \mathtt{One(0)} = w_1) ここから、\vec{w} は行列 P の 1 番目の行のインスタンスではありません。
3. ベクトル \vec{z} = (\mathtt{One(1)}, \mathtt{One(1)}) は P の 5 番目の行にマッチします。
   • ベクトル \vec{z} は \vec{p^5} = (\mathtt{\_}, \mathtt{\_}) のインスタンスです（このパターンは型 mylist のあらゆる値にマッチします）。
   • くわえて、ベクトル \vec{z} はその他のいずれのパターンにもマッチしません。たとえば、\mathtt{0} \npreceq \mathtt{1} なので \mathtt{One(0)} \npreceq \mathtt{One(1)} となり、ベクトル \vec{z} は 3 番目と 4 番目のパターンにはマッチしません。

すでに述べたようにパターンはそのインスタンスの集合として考えることができます。同じように、パターンの行列は各行のインスタンス集合の和集合である、と考えることができます。

定義 3. 行列におけるインスタンス関係

P を n 個の列と m 個の行をもつパターンの行列だとし、値ベクトルを \vec{v} = (v_1 \cdots v_n) とします。行番号 i (i \in [1 \dots m]) の行が以下の条件を満たすとき、ベクトル \vec{v} は行列 P のインスタンスであるといい、これを P \preceq \vec{v} と書きます。

ML 言語のパターンマッチングはこの新しい定義によって以下のように定式化できます。P^{[1 \dots i]} \npreceq \vec{v} かつ \vec{p^i} \preceq \vec{v} のとき、\vec{v} は行列 P の i 番目の行にマッチします。ここで、行列 P^{[1 \dots i]} は、P の行番号 i より前の行からなる (i - 1) \times n の行列だとします。

3. The useful clause problem

ここからは、パターンマッチングにおける異常を行列の枠組みで定義します。

定義 4. 網羅性 Exhaustiveness

パターン行列 P は、適切な型のすべての値ベクトル \vec{v} について、定義 2 の意味で \vec{v} をフィルタリングする行が P に存在する場合にかぎり、網羅的 (exhaustive) である、といいます。

定義 5. 無効な節 Useless clause

パターン行列 P の i 番目の行は、定義 2 の意味でマッチする値ベクトル \vec{v} が存在しない場合、無効 (useless) である、といいます。無効な行は冗長 (redundant) である、といわれることもありますが、useless の方がより正確であり、概念の意味的な性質をよりよく伝えていると思われるので、本稿ではこちらの用語を用います。

例 2

次のようなパターン行列 P と Q があるとします。型は mylist です。

行列 P は網羅的ではありません。なぜなら、たとえば、\vec{v} = (\mathtt{One(0)}, \mathtt{One(0)}) がいずれの行にもマッチしないからです。

一方、行列 Q は網羅的です。型 mylist がとりうる値を考えてみましょう。v_1 と v_2 は \mathtt{Nil}, \mathtt{One(\_)}, または \mathtt{Cons(\_, \_)} のインスタンスです。つまり、値を 9 つの異なるパターン・ベクトルで示される 9 つの組み合わせに分割することができます。これらの組み合わせだけで、定義2を適用するのに十分であることがわかります。

Q の 6 番目の行が無効であることもわかります。

ここでは，パターン・マッチングの ML 言語での定義（定義 2）を用いており、上記の定義 4, 5 は，一般的に理解されている「網羅的なマッチ」と「無効な節 clause」を表しています。しかし、この 2 つの問題が非常に似ていることは直感的に明らかであり，実際には以下のような定義で表現することができます。

定義 6. 有効な節 Useful clause

P をサイズ m \times n のパターン行列とし、\vec{q} をサイズ n のパターンベクトルとします。ベクトル \vec{q} が行列 P に対して有効であるのは、以下の場合に限られます。^[1]

上記の式を \mathcal{U}(P, \vec{q}) と書き、マッチする値の集合を \mathcal{M}(P, \vec{q}) とします。

つまり、\mathcal{U}(P, \vec{q}) は \mathcal{M}(P, \vec{q}) が空ではない、ということです。

命題 1

1. \mathcal{U}(P, \_ \cdots \_) が偽なら、行列 P は網羅的である
2. \mathcal{U}(P^{[i\dots i)}, \vec{p^i}) が偽なら、行列 P の行番号 i は無効である

証明

定義のとおり。

ふたつの定義 2 と 3 より、パターンマッチングの異常性に関する限り、マッチング述語が単純化できることがわかります。より正確には、\vec{v} が P のある行にマッチすること（定義 2）は、P \preceq \vec{v}（定義 3）と同等であることに気づくことが重要です。つまり、\mathcal{U}(P, \vec{q}) を計算する際に、P の行の順番は関係ありません。

3.1 Solving the useful clause problem

このセクションでは \mathcal{U} を再帰的に計算していきます。まず、再帰関数 \mathcal{U}\mathrm{rec} を定義し、次に \mathcal{U}=\mathcal{U}\mathrm{rec} であることを示します。\mathcal{U}\mathrm{rec} の定義は、ML 言語のパターンマッチングを決定木にコンパイルする伝統的な手法に多くを依っています。この古典的な手法に現代的な表現を与えます。

そこで、P をサイズ m \times n のパターン行列、\vec{q} をサイズ n のパターンベクトルとします。ここからは、P と q を第 1 列に沿って分解することで帰納的に解いていきます。

基底ケース 列がひとつも存在しない場合 (n = 0) 、\mathcal{U}\mathrm{rec}(P, ()) は行列 P の行数 m に依存します。^[1]

1. P が行をもつ (m \gt 0) 場合、\mathcal{U}\mathrm{rec}(\begin{pmatrix}&\\&\end{pmatrix}, ()) は false です
2. m = 0 の場合、\mathcal{U}\mathrm{rec}(\emptyset, ()) は true です。不要ではありますが、より一般的には、\mathcal{U}\mathrm{rec}(\emptyset, \vec{q}) はあらゆるサイズ n の \vec{q} で true になります。

以上をまとめるとこうなります。

帰納 列が存在する場合 (n \gt 0)、q_1 の性質に応じて 3 つのケースに分かれます。

1. q_1 がコンストラクタパターンの場合

パターン q_1 がコンストラクタパターン q_1 = c(r_1, \dots r_a) の場合。行列 P から特殊化 (specialized) した行列 S(c, P) を作ります。この新しい行列 S(c, P) は a + n - 1 の列をもち、行は P の各行によって定義されます。このときの各行の第 1 列目を見てみると、以下のようになります。

与えられた行 \vec{p^i} は、S(c, P) の 0 個以上の行になる可能性があることに注意してください。

以下の S(c, \vec{q}) は、S をベクトルに適用すると、ベクトルが得られることを示しています。

また、v_1 = c(w_1, \dots ,w_a) のとき、値ベクトルの特殊化も考慮します。

最後に、q_1 が c(r_1, \dots , r_a) のとき、次のように定義します。

2. q_1 がワイルドカードパターンの場合

\Sigma = \{c_1,c_2, \dots ,c_z\} を、P の第 1 列のパターンのルート・コンストラクタとして現れるコンストラクタの集合とします（また、第 1 列のパターンが or パターンの場合は、それぞれのパターンのルート・コンストラクタの集合）。

\mathcal{U}\mathrm{rec} の計算は集合 \Sigma に上限と下限が存在するかどうかに依存します。

集合 \Sigma に上限と下限が存在する場合、\vec{q} のインスタンス \vec{v} は、第 1 要素のルート・コンストラクタが \Sigma に属しているはずです。

集合 \Sigma に上限と下限が存在しない場合、\vec{q} のインスタンス \vec{v} は、第 1 要素のルート・コンストラクタが \Sigma に属していないことが分かれば十分です。

この通り、\mathcal{U}\mathrm{rec} の計算は決定木へのコンパイルから大きく逸脱しており、すべてのコンストラクタを考慮しなければなりません。

(a) 集合 \Sigma に上限と下限が存在する場合 ^[2]

(b) 集合 \Sigma に上限と下限が存在しない場合

パターン行列 P から、幅 n - 1 のデフォルト (default) 行列を作ります。

行列 \mathcal{D}(P) はどのパターンに対しても定義することができますが、集合 \Sigma に上限と下限が存在する場合のみ \mathcal{U}\mathrm{rec} の計算に役立ちます。

\Sigma が空のとき、すなわち、P の第 1 列がワイルドカード、またはワイルドカードを伴う or-パターンの場合、\Sigma には上限も下限も存在しないことに注意してください。これも (b) に相当します。

3. q_1 が or-パターン (r_1 \mid r_2) の場合

ここで、行列の特殊化 (以下の 1) とデフォルト行列 (以下の 2 から 4) のいくつかの「重要な」特性を証明していきます。

基本的に、特殊化の重要な特性は、第一成分に c をルートコンストラクタとしてもつ値ベクトルについて、P によるマッチングとS(c,P) によるマッチングが等価であることであり、一方、デフォルト行列の重要な特性は、より詳細に見ていくと、P によるマッチングと \mathcal{D}(P) によるマッチングが等価であることです。

補題 1 (重要な特性)

任意の行列 P、コンストラクタ c、値ベクトル \vec{v} にたいして、v_1 = c(w_1, \dots , w_a) (すべて適切な型である) であれば、次のようになります。

任意の値ベクトルについて、

更に、任意の行列 P について、\Sigma を P の第 1 列のルート・コンストラクタの集合とします。\Sigma が空でない場合、\Sigma に属さない任意のコンストラクタ c と任意の値ベクトル (w_1 \cdots w_a \; v_2 \cdots v_n) において、

であり、逆に \Sigma が空の場合、任意の値ベクトル \vec{v} において、

になります。

証明

定義による。

上記では、\npreceq の代わりに \preceq を使って、主要な特性を定式化することも可能です。しかし、ここでは定義 2 に合わせて、否定の形で表現しています。ただし、P が 1 行のときにも (1) を考えます。その場合、v_1 = c(w_1, \dots , w_a) となるような任意の値ベクトル \vec{v} についてより直接的に書句ことができます。

命題 2

任意の行列 P と適切なサイズと型のパターン・ベクトル \vec{q} があるとき

証明

（省略）

3.2 Detecting the anomaries

ここまでで \mathcal{U} を計算する方法は分かったので、パターンマッチの異常を検出することができます。\texttt{match} \; \dots \; \texttt{with} \; p_1 \;\texttt{->} \; e_1 \mid p_2 \; \texttt{->} \; e_2 \mid \; \dots \mid p_m \; \texttt{->} \; e_m, という式があるとき、網羅性は以下のように計算できます。

更に、i 行目の節の有効性は以下のように計算できます。

PART 2 Implementation

5. 網羅性チェックのための \mathcal{U} の特殊化

網羅性チェックにおいて、単に「ありうるパターンが網羅されていない」と警告するだけではプログラマを困惑させるだけでしょう。しかし、警告とともに「マッチしない値」の例があれば「確かに、マッチしないパターンを書いてしまった」と納得してもらえるだけでなく、コードを修正するのにも大いに役立ちます。

このような例（または反例）は、マッチしない例の集合を表すパターンとして表現するのが最適です。プログラマーは、この「反例」をパターンマッチの最後に追加することで、パターンが網羅的になることを期待します。簡単な例を挙げてみましょう。

let nilp = function [] -> true
Warning: this pattern-matching is not exhaustive.
Here is an example of a non-matching value:
_::_

与えられたパターンマッチングは網羅的ではなく、パターン \texttt{\_::\_} (リストセル)のすべてのインスタンスを網羅していません。ここでは、最後にパターン \texttt{\_::\_} を持つ節を追加することで、網羅的なマッチにできます。

これらの例は、アルゴリズム \mathcal{U} にちょっとした拡張を施すことで簡単に計算することができます。実際、アルゴリズム \mathcal{U} は \mathcal{M}(P, \vec{q}) が空でないことを計算する過程で、これらの例も計算しているのです。

新しいアルゴリズム \mathcal{I} を考えましょう。これは行列 P と整数 n を引数として取ります。\mathcal{I} は第 3.1 節のパターン・ベクトル \vec{q} が n 個のワイルドカードパターンであるときに使われます。アルゴリズム \mathcal{I} は通常、サイズ n のパターン・ベクトル \vec{p} を返し、\vec{p} のインスタンスが「マッチしない値の集合」になります。もし、そのような値が存在しない場合（つまり、P が網羅されている場合）、\mathcal{I} は \perp という定数を返します。

基底ケース

まず、n = 0 のとき、

であり、より一般的には、\mathcal{I}(\empty, n) は n 個のワイルドカードで構成されたベクトルになります。

帰納

n \gt 0 の場合、\Sigma をパターン行列 P の第 1 列のルート（または or-パターンの場合、それぞれのルート）に現れるコンストラクタの集合とします。

1.集合 \Sigma に上限と下限が存在する場合

集合 \Sigma に上限と下限が存在する場合、\Sigma に含まれるすべてのコンストラクタ c_k について、再帰的にアルゴリズ \mathcal{I} を適用し、\mathcal{I}(S(c_k, P), a_k + n - 1) を計算します。

もし、すべての計算結果が \perp であれば、\mathcal{I}(P, n) の結果もまた \perp です。

そうではなく、\mathcal{I}(S(c_k, P), a_k + n - 1) がパターン・ベクトル (r_1 \cdots r_{a_k} \; p_2 \cdots p_n) を返した場合、 \mathcal{I}(P, n) = (c_k(r_1, \dots, r_{a_k}) \; p_2 \cdots p_n) です。もちろん、実際には、結果が見つかり次第、そこでアルゴリズムの再帰的な適用をストップします。同様に \mathcal{I}(S(c_{k'}, P), a_{k'} + n - 1) がパターン・ベクトルを返す c_{k'} がありうるため、アルゴリズム \mathcal{I} は非決定的です。

2.集合 \Sigma に上限と下限が存在しない場合

まず、\mathcal{I}(D(P), n - 1) だけを計算します。結果が \perp であれば、\mathcal{I}(P) = \perp です。そうではなく、\mathcal{I}(D(P), n - 1) がベクトル (p_2 \cdots p_n) を返す場合、\mathcal{I}(P) の結果は \Sigma が空かどうかに依存します。もし、\Sigma が空の場合、\mathcal{I}(P) = (- p_2 \cdots p_n) です。\Sigma が空でない場合、\mathcal{I}(P) = (c(\_, \dots, \_) \; p_2 \cdots p_n) であり、c は、c_k でなくても、c_k のシグネチャからのコンストラクタです。c_k のシグネチャが有限であまり大きくない場合は、余分なコンストラクタをすべて含む or-パターンを使用することもできます。

\mathcal{I}(P, n) = \perp である場合に限り、P が網羅的であることは明らかです。それ以外では、\mathcal{I}(P, n) の結果は何らかのパターン・ベクトル \vec{p} となり、\vec{p} のインスタンスがマッチしない値となります。

簡単な例でアルゴリズム \mathcal{I} の動きを見てみましょう。第 2 節に出てきた mylist 型の値にマッチするパターンマッチの網羅性をチェックするとします。

match ... with One 1 -> ...

従って、ここでは \mathcal{I}((\mathtt{One} \; \mathtt{1}), 1) を計算します。

ここで、特殊化された行列を再帰的に計算し、すべてのありうるパターン・ベクトルを導き出せばいいのではないか、と思う人もいるかもしれません。しかし、たとえば、整数を考えてみても、それの取りうる値は無限に存在するため、これが不可能なことが分かります。また、実際のところ、マッチしない例をひとつ示すだけで十分です。警告の原因となったコードを修正するのはプログラマの責任であり、コンパイラはできるだけコストをかけずに適切な警告を提供するだけでいいのです。上記の例では、(\texttt{Nil|Cons (\_, \_)}) が最も明らかな見過ごされたパターンになります。さらに、このように示されたパターンを追加してプログラムをリコンパイルすれば、コンパイラはまた新しいパターン（\texttt{One 0} など）を提供することができます。プログラマが望むなら、この手順を繰り返せばいいわけです。

6. 無効な節チェックのための \mathcal{U} の特殊化

一見すると無効な節チェックのためにはアルゴリズム \mathcal{U} そのままで十分に思えます。実際のところ、リコンパイルせずに無効な節をなくしたいプログラマにとって簡潔で有用な情報を与えることはできません。また、or-パターンは無効な節に関連した特有の問題をもたらします。

mylist 型 (Section 2) の値のうち、最初の要素が 1 かどうかを判別する関数を書いているとしましょう。

let f = function
| One x | Cons (x,_) -> x=1
| Nil | One _ | Cons (_,_) -> false

直感的に何かがおかしいことに気づきますね。最後のパターンは必要以上に複雑に見えます。そして、実際に、次のコードの方がより簡潔です。

let f = function
| One x | Cons (x,_) -> x=1
| Nil  -> false

残念ながら、アルゴリズム \mathcal{U} は最初のコード例をそのまま受け入れてしまいます。良いコンパイラは最初のコード例をより "良い" ２番目のコードで置き換えるようにアドバイスするべきです。

そして、or-パターンが展開された次のコードであれば、アルゴリズム \mathcal{U} も期待されたように動作します。

let f = function
| One x | Cons (x,_) -> x=1
| Nil -> false
| One _ -> false
| Cons (_,_) -> false

この場合、コンパイラは最後のふたつのパターンが無効であることを検知できるので、プログラマはこれらを削除することができます。

では、最初の例ではどうして検知できなかったのでしょうか？

let f = function
| One x | Cons (x,_) -> x=1
| Nil | One _ | Cons (_,_) -> false

Nil | One _ | Cons (_,_) -> false 節は Nil が含まれており、このために「有用である」と判定されています。しかし、それ以外の One _, Cons (_, _) は冗長であり、削除しても関数 f の挙動は変わりません。さらに、こうした冗長なパターンの定義は、or-パターンを展開することによって簡単に構築することができます。

実際のところ、Objective Caml のコンパイラが警告を出すときも、冗長な節 自体ではなく、冗長なパターンそれぞれについて警告を出すようになっています。

let f = function
| One x | Cons (x,_) -> x=1
| Nil | One _ | Cons (_,_) -> false
        ^^^^^   ^^^^^^^^^^
Warning: this pattern is unused.
Warning: this pattern is unused.

コード中には多くの or-パターンが含まれる可能性があるため、そのうちのひとつを展開することでコードサイズが指数的に増えることを防ぎます。例えば、以下のようなコードだと、

let f = function
| (1|2), (3|4), (5|6), ..., (2k−1|2k) -> true
| _ -> false

or-パターン (2k−1|2k) をチェックするためには、以下のようにひとつだけ展開するので十分です。

let f = function
| (1|2), (3|4), (5|6), ..., 2k−1 -> true
| (1|2), (3|4), (5|6), ..., 2k -> true
| _ -> false

既知のアルゴリズ \mathcal{U} により、パターン 2k-1 と 2k は有効であると断言できます。逐次的な展開を行うことで、指数的なコードサイズの増加もありません。

or-パターンの展開では、(p_1 \mid p_2) を展開するときに左側の p_1 を右側の p_2 よりも優先するようにします。左から右への展開をすることによって、以下のような境界例のチェックが明確になります。

let f1 = function (1|_) -> true
and f2 = function (_|1) -> true
and f3 = function (1|1) -> true
and f4 = function (_|_) -> true

展開してみると分かるように、or-パターンの右側の選択肢は、f1 では有効ですが、それ以降は無効です。

let f1 = function 1 -> true | _ -> true
and f2 = function _ -> true | 1 -> true
and f3 = function 1 -> true | 1 -> true
and f4 = function _ -> true | _ -> true

良い診断結果を出すためには「or-パターン引数のマッチングを試みる順序を指定しない（ただし、Haskell のマッチングは違います）」という定義を見直さなければいけない、と思うかもしれません。しかし、実際には、正格かつ Laville のマッチングでは、このような順序を指定する必要はありません。これらのパターンマッチングの定義は、どの行がマッチングされるかに依存し、どのようにマッチングされるかには依存しません。とはいえ、実際には、診断結果と生成されたコードの一貫性を保つため（or-パターンに変数があるため、実行するとマッチした選択肢が見えてしまいます）、コンパイラは左から右への順序を考慮しなければなりません。これは、SML/NJ コンパイラ (Appel & MacQueen, 1991) などパターンマッチの前に展開を実行するコンパイラのように、パターンマッチの過程で展開を実行する（正格な）コンパイラ (Le Fessant & Maranget, 2001) でも、容易に達成できます。

次のセクションではアルゴリズ \mathcal{U} の改良版について説明します。この改良は、無効なパターンを見つけることを目的とし、or-パターンの展開に依存しています。予備知識として、この改良を施してもアルゴリズ \mathcal{U} の出力は変わらないことに注目します。

定理 4 (パターン展開の有用性)

3 つすべてのパターンマッチの定義において、

ここで P@\vec{p} は行列 P の末尾に行ベクトル \vec{p} を追加したものとします。

証明

（割愛）

6.3 Rules for finding useless patterns

TBD

6.4 Computation of useless patterns

TBD

https://github.com/rust-lang/rust/blob/d331cb710f0dd969d779510a49a3bafc7f78a54e/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs

パターンマッチの検証では、ある型に対するパターンのリストが与えられたとき、以下を判定するアルゴリズムが必要。

• (a) それぞれのパターンが到達可能かどうか reachability
• (b) パターンがすべてのありうる値をカバーしているかどうか exhaustiveness

アルゴリズムの核は usefulness

• 同じ型のパターン p と q があり、q にマッチし p にマッチしない値があるとき、q は p と比べて useful である
• これは複数の p に対しても一般化される
  • 同じ型のパターン p_1, p_2 ... p_n があり、q にマッチし p_i にマッチしない値があるとき、q は p と比べて useful である
  • usefulness(p_1 .. p_n, q) はそのような値 (witness) のリストを返す関数
• usefulness 関数があれば reachability は計算可能
  • あるパターンは、それよりも前のパターンすべてに関して useful であれば到達可能である

match x {
  Some(_) => ...,
  None => ..., // 到達可能。None がこのパターンにマッチする
  Some(0) => ..., // 到達不可能。このパターンがマッチするすべての値は、すでに Some(_) でマッチ済みである
}

exhaustiveness も計算可能

• あるマッチは、ワイルドカードパターン _ が usefull でなければ exhaustive

match x {
  Some(0) => ...,
  None => ...,
  // 網羅的ではない。ワイルドカードパターン _ が useful (Some(1) にマッチするので)
}

compute_match_usefulness 関数

• それぞれのブランチの到達可能性
• すべてのマッチの網羅性

コンストラクタとフィールド

• ctor = constructor の略
• あらゆる値はコンストラクタをいくつかの引数（フィールド）に適用することで生成される
  • 例: Some, None
  • (,) 2 要素タプル
  • Foo{...} Foo 構造体のコンストラクタ
  • 2 数値 2 のコンストラクタ
  • None や 2 は引数（フィールド）をひとつも取らないコンストラクタ
• こうすることで、あらゆる値はコンストラクタの木構造で表すことができる。
  • 例えば、Foo { bar: None, baz: Ok(0) } は Foo, None, Ok , 0 で構成されている

• パターンも同様
  • すべての値コンストラクタに加えて、パターン特有のコンストラクタもある
  • たとえば、ワイルドカード _
  • 整数 Range 0..=10
  • 任意長のスライス [x, ..]
  • Or-パターン Ok(0) | Err(_)
  • 変数を束縛するパターン (e.g. Some(x)) はワイルドカードと同義
• ある値があるパターンにマッチするかどうかは、コンストラクタをひとつずつ見ていく。
  • パターン p と値 v が与えられたとき matches!(v, p) を計算する
    • 先頭のコンストラクタを比較して、同じであれば、そのフィールドを再帰的に比較していく。

典型的な例

matches!(v, _) // true
matches!((v0,  v1), (p0,  p1)) // matches!(v0, p0) && matches!(v1, p1)
matches!(Foo { bar: v0, baz: v1 }, Foo { bar: p0, baz: p1 }) // matches!(v0, p0) && matches!(v1, p1)
matches!(Ok(v0), Ok(p0)) // matches!(v0, p0)
matches!(Ok(v0), Err(p0)) // false - incompatible variants
matches!(v, 1..=100) // matches!(v, 1) || ... || matches!(v, 100)
matches!([v0], [p0, .., p1]) // false - incompatible length
matches!([v0, v1, v2], [p0, .., p1]) // matches!(v0, p0) && matches!(v2, p1)
matches!(v, p0 | p1) // matches!(v, p0) || matches!(v, p1)

• コンストラクタ、フィールドと関連する操作は super::deconstruct_pat モジュールにある
• Note: このコンストラクタ、フィールドの定義はすべての Rust の型に適用できるわけではない
  • Rc<u64> はこの方法では分解できない
  • &str は無限のコンストラクタを持つことになる
  • 他にもいろいろ微妙な点は多い
  • ただ、コンストラクタのアイデアはこれらを処理できるように拡張可能である
• コンストラクが他のコンストラクタをカバーできるかどうかは Constructor::is_covered_by で判定できる

Specialization

• usefulness(p_1 .. p_n, q) を計算したい
• p_1 .. p_n と q が与えられた時に、q にマッチし、p_i にマッチしない値
  • これらの値を witnesses と呼ぶ
• とはいえ、すべてのありうる値を列挙するわけではない

前段の話の通り、与えられた型を構成するコンストラクタをひとつずつ見ていくことになる。ここで見るのは、それぞれの値コンストラクタにおいて、このコンストラクタから始まり、パターン q にマッチし、かつ、パターン p_i にマッチしない値があるかどうか、である。以前にも分かった通り、候補となる値の最初の (つまり、木構造のルートの) コンストラクタを見るだけでも、多くのことが分かる。

match x {
    Enum::Variant1(_) => {} // `p1`
    Enum::Variant2(None, 0) => {} // `p2`
    Enum::Variant2(Some(_), 0) => {} // `q`
}

ここに候補となる値 v があるとき、v が Variant1 から始まるのであれば q にはマッチしない。しかし、もしも v が v = Variant2(v0, v1) であれば、p2 か q にマッチする可能性があり、それは v0 と v1 の値次第である。実際、値 v が q の usefulness を判定するときの witness になるのは、タプル (v0, v1) が以下のような簡略化されたコードにおいて q の witness になるときである。

match x {
    (None, 0) => {} // `p2'`
    (Some(_), 0) => {} // `q'`
}

これが、usefulness の計算において、我々が specialization (特殊化) と呼ぶ新しいステップを導入した理由である。

特殊化のステップでは、値コンストラクタにマッチするパターンのリストをフィルタリングしてから、コンストラクタのフィールドを調べます。これにより、usefulness を再帰的に計算することができます。

各行の単一のパターンを処理するのではなく、各行のパターンのリストを考えることにし、そのようなリストを_pattern-stack_と呼ぶことにします。

• pattern-stack は先頭のコンストラクタを pop して、そのフィールドを push したり、
• pop したコンストラクタを push し直して、元に戻したりすることができます。

pattern-stack を単に [p_1 ... p_n] と記すことにします。ここでは、何が起こっているかを説明するために、パターン・スタックのリストの特殊化のシーケンスを示します。

以下のような pattern-stack のリスト (Matrix) があったとして、

[Enum::Variant1(_)]
[Enum::Variant2(None, 0)]
[Enum::Variant2(Some(_), 0)]

これを Variant2 に対して特殊化します。

[None, 0]
[Some(_), 0]

Some に対して特殊化します。

[_, 0]

タプルの最初の要素の型が bool だとして、_ に対して特殊化します。

[0]

最後に、0 に対して特殊化します。

[]

関数 specialize(c, p) は値コンストラクタ c とパターン p を受け取り、0 個以上の pattern-stack を返します。

• もし、値コンストラクタ c とパターン p の最初のコンストラクがマッチしない場合は何も返しません。
• そうでなければ、コンストラクタのフィールドを返します。
• ひとつ以上の pattern-stack を返すのは、p がパターン特有のコンストラクタを持つときのみです。

さらに、以下のようなケースがあります。

誤ったコンストラクタの特殊化は何も返しません。

specialize(None, Some(p0)) // []

正しいコンストラクタの特殊化は単一の行にコンストラクタのフィールドを含む Matrix を返します。

specialize(Variant1, Variant1(p0, p1, p2)) // [[p0, p1, p2]]
specialize(Foo{..}, Foo { bar: p0, baz: p1 }) // [[p0, p1]]

Or-パターンに対しては、それぞれの分岐を特殊化し、結果を結合します。

specialize(c, p0 | p1) // specialize(c, p0) ++ specialize(c, p1)

同様に、他のパターンコンストラクタも、ありうるパターンすべてを列挙した Or-パターンのように扱います。

specialize(c, _) // specialize(c, Variant1(_) | Variant2(_, _) | ...)
specialize(c, 1..=100) // specialize(c, 1 | ... | 100)
specialize(c, [p0, .., p1]) // specialize(c, [p0, p1] | [p0, _, p1] | [p0, _, _, p1] | ...)

もしも、コンストラクタ c がパターン特有のコンストラクタの場合は、specialize 関数はそれぞれの場合わけで実装されています。

また、この関数は pattern-stack を入力として取るように拡張されています（各行の最初のカラムのみ処理し、他の要素は変更しない）。

• Matrix を処理する特殊化は Matrix::specialize_constructor で実装されています。ただし、最初のカラムが Or-パターンの場合は matrix に格納される前に展開されます。
• 単一の pattern-stack を処理する特殊化は、Constructor::is_covered_by と PatStack::pop_head_constructor を組み合わせて実装されています（Fields 構造体に詳しい）

usefulness の計算

これで usefulness を計算できる

• 入力
  • pattern-stack p_1 ... p_n のリスト (ただし、1行にひとつ)
  • 新しい pattern-stack q
  • なお、pattern-stack のリストを matrix と呼ぶ
  • これらはすべて同じ数の列を持ち、与えられた列の中のパターンはすべて同じ型でなければなりません
• usefulness は witness のリスト（空かもしれません）を pattern-stack で返します。
• base case: n_columns == 0
  • 空の pattern-stack は Unit type () のようなもの
  • したがって、qはその上に行がない場合、つまり n == 0 の場合に useful です
• inductive case: n_columns > 0
  • 試してみたいコンストラクタをリストアップする方法が必要です。ここでは最初の列の型に対するすべての値のコンストラクタをリストアップするものとします。次の節でもっとスマートな方法を紹介します。

手順

• それぞれのコンストラクタ c について
  • それぞれのパターン q について specialize(c, q) の返り値 q' について
    • usefulness(specialize(c, p_1) ... specialize(c, p_n), q') を計算する
  • それぞれの見つかった witness について、c を push し直して特殊化を "revert" します
• 見つかった witness をひとつのリストに結合して返します。

例

[Some(true)] // p_1
[None] // p_2
[Some(_)] // q
//==>> try `None`: `specialize(None, q)` returns nothing
//==>> try `Some`: `specialize(Some, q)` returns a single row
[true] // p_1'
[_] // q'
//==>> try `true`: `specialize(true, q')` returns a single row
[] // p_1''
[] // q''
//==>> base case; `n != 0` so `q''` is not useful.
//==>> go back up a step
[true] // p_1'
[_] // q'
//==>> try `false`: `specialize(false, q')` returns a single row
[] // q''
//==>> base case; `n == 0` so `q''` is useful. We return the single witness `[]`
witnesses:
[]
//==>> undo the specialization with `false`
witnesses:
[false]
//==>> undo the specialization with `Some`
witnesses:
[Some(false)]
//==>> we have tried all the constructors. The output is the single witness `[Some(false)]`.

これらの処理は is_useful 関数にあります。

実際には、到達可能性を計算するときに witness のリストは必要ありません。witness が存在するかどうかだけを知る必要があります。 witness のリストは、網羅性を計算するときに、ユーザーに報告するために使います。

Constructor splitting

usefulness アルゴリズムで、値コンストラクタを列挙するとき、

• 単純にすべてのあり得る値を列挙するのは非現実的
  • u64 や &str でどうなるか...
• まず、パターン q の先頭のコンストラクタがカバーする値コンストラクタを列挙すれば十分である
  • 先頭のコンストラクタが値コンストラクタであれば、それだけで良い
  • パターンコンストラクタであれば、Constructor splitting という手法でコンストラクタ群をグループ分けする

https://github.com/rust-lang/rust/blob/1b3a5f29dd9f9ba9de0d501857d4603a54e15707/compiler/rustc_mir_build/src/thir/pattern/deconstruct_pat.rs#L9

コンストラクタ c と matrix (pattern-stack のリスト) が与えられたとき、 c がカバーするすべての値のコンストラクタを順番に特殊化し、それぞれについて usefulness を計算したい。すべてのコンストラクタを列挙するのは困難なので、それらの値のコンストラクタを可能な限りグループ化します。

match (0, false) {
    (0 ..=100, true) => {} // `p_1`
    (50..=150, false) => {} // `p_2`
    (0 ..=200, _) => {} // `q`
}

上記のコードで q を特殊化するとき、素朴な方法では、0..=200 の範囲にあるすべての数を試すことになります。

しかし、例えば 0 と 1 は全く同じ行にマッチし、同等の witness が返されます。実際、0..50はすべてそうなります。このように、4つのコンストラクタに限定して探索することができます。0..50, 50..=100, 101..=150, 151..=200 の4つのコンストラクタに絞ることができます。これで十分であり、限りなく扱いやすいものです。

関数 split(p_1 ... p_n, c) は、 c がカバーするコンストラクタ c' のリストを返します。 c' がカバーするすべての値コンストラクタ c'' は、特殊化して usefulness を計算すると、同等の witness のセットを返すことを要求します。上の例では、 0..50 がカバーする c'' によって特殊化した場合の witness は、その最初の要素だけが異なることになります。

また、通常は c' を合わせて、元の c をすべてカバーすることを求めます。しかし、結果として得られる witness のリストが空であるかどうかを変えない限り、いくつかのコンストラクタをスキップすることを許可しています。これはワイルドカードの _ の場合に使用します。

Constructor splitting は Constructor::split 関数で実装されています。Or-パターンの分割は行いません。その代わり、選択肢を1つずつ試していきます。ワイルドカードの分割については SplitWildcard を、整数の範囲については SplitIntRange を、スライスについては SplitVarLenSlice を参照してください。

usefulness.rs atcompiler/rustc_mir_build/src/thir/pattern/usefulness.rs

• compute_match_usefulness()
  • usefulness アルゴリズムのエントリーポイント
  • 入力となる arm の各パターンはあらかじめ MatchVisitor::lower_pattern() でコンストラクタとフィールドの組 (DeconstructedPat) に変換しておく必要がある。

deconstruct_pat.rs at compiler/rustc_mir_build/src/thir/pattern/deconstruct_pat.rs

• Constructor::split() - constructor splitting の実装
  • ワイルドカード
  • 整数パターン
  • （可変長）配列パターン
• IntRange
  • 整数またはその範囲パターン
    • 2, 2..=5 or 2..5
  • 整数のリテラルパターンも含まれることに注意