6マッチャーを定義しよう

本章は，ユーザーが自身でマッチャーを定義する方法を解説する．

6.1inductive pattern宣言

マッチャーを定義する際には，そのマッチャーが処理するパターンコンストラクタをあらかじめinductive pattern宣言（inductive pattern declaration）で宣言しておく必要がある．

inductive pattern宣言は，パターンコンストラクタの型を，データコンストラクタやマッチャーの定義から独立して宣言するための構文である． たとえば，リスト型[a]に対するパターンコンストラクタは以下のように宣言される．

inductive pattern [a] :=
  | []
  | (::) a [a]
  | (++) [a] [a]

この宣言は，パターンコンストラクタ[]，::，++がいずれもリスト型[a]を対象とするパターンコンストラクタであることを宣言している． 各パターンコンストラクタの後に並ぶ型は，そのパターンコンストラクタの引数の型，すなわちパターンマッチの成功時にネクスト・ターゲットとして渡される値の型を表す．

inductive pattern宣言の重要な特徴は，::というパターンコンストラクタがlistマッチャー，multisetマッチャー，setマッチャーなど，複数のマッチャーにわたって共有される点にある．それぞれのマッチャーは::に対して異なる分解方法を実装するが，そのパターンコンストラクタの型はinductive pattern宣言によって一元的に管理される．

matchAll [1, 2, 3] as list integer with
  | $x :: $xs -> (x, xs)
-- [(1,[2,3])]

matchAll [1, 2, 3] as multiset integer with
  | $x :: $xs -> (x, xs)
-- [(1,[2,3]),(2,[1,3]),(3,[1,2])]

同じパターン$x :: $xsでも，使うマッチャーによって意味（分解方法）が変わる．

このinductive pattern宣言とマッチャー定義の関係は，型クラスとインスタンス定義の関係に類似している． 型クラス宣言がメソッドの型を宣言し，インスタンス定義がその具体的な実装を提供するのと同様に，inductive pattern宣言がパターンコンストラクタの型を宣言し，マッチャー定義がそのパターンコンストラクタに対する具体的な分解方法を定義する．

型クラスパターンマッチング
型クラス宣言inductive pattern宣言
インスタンス定義マッチャー定義
メソッド名パターンコンストラクタ名
メソッドの型パターンコンストラクタの型
インスタンスディスパッチ（静的）マッチャーディスパッチ（動的）

ただし，型クラスのインスタンス選択がコンパイル時に静的に決定されるのとは異なり，マッチャーの選択はmatch式やmatchAll式においてユーザーが実行時に明示的に指定する（動的選択）．

6.2マッチャーの定義の基礎

本節は，非自由データ型のなかでもっとも単純なunordered pair（要素の順番を無視するペア）のマッチャー定義をみていくことにより，マッチャー定義の方法の概略を解説する．

まずは，整数のunordred pairに対するマッチャーunorderedIntegerPairマッチャーの挙動を確認しよう． unorderedIntegerPairに対して，pairパターンを使うと以下のように2通りの要素の順番を両方パターンマッチする．

matchAll (1, 2) as unorderedIntegerPair with
| pair $x $y -> (x, y)
-- [(1,2),(2,1)]

そのおかげで，pairの第一引数がターゲットの2番目の要素である場合にも，パターンマッチに成功する．

matchAll (1, 2) as unorderedIntegerPair with
| pair #2 $y -> y
-- [1]

パターンがパターン変数であった場合には，ターゲットをそのまま束縛する．

matchAll (1, 2) as unorderedIntegerPair with
| $p -> p
-- [(1,2)]

上記のような動作をするunorderedIntegerPairマッチャーは以下のように定義できる． まず，pairパターンコンストラクタをinductive pattern宣言で宣言しておく必要がある．

inductive pattern (Integer, Integer) :=
  | pair Integer Integer

この宣言は，pairが整数のペア型(Integer, Integer)を対象とするパターンコンストラクタで，Integer型の引数を2つ取ることを宣言している． 次に，型注釈により整数のペアに対するマッチャーであることを示しながら，unorderedIntegerPairマッチャーを以下のように定義する．

def unorderedIntegerPair : Matcher (Integer, Integer) := matcher
  | pair $ $ as (integer, integer) with
    | ($x, $y) -> [(x, y), (y, x)]
  | $ as something with
    | $tgt -> [tgt]

matcherは，マッチャーを生成するための組み込み構文である．

matcher
| `primitive pattern-pattern` as `next matcher expression` with
  | `primitive data pattern` -> `body`
  ...
...

matcher式は，複数のマッチャー節（matcher clause）をとる． マッチャー節は，原始パターンパターン（primitive pattern-pattern），ネクスト・マッチャー式（next matcher expression），複数の原始マッチ節（primitive match clause）からなる． 原始マッチ節は，原始データパターン（primitive data pattern）とボディからなる．

unorderedIntegerPairの1つ目のマッチャー節（2-3行目）をみていく． まず，このマッチャー節の原始パターンパターンはpair $ $である． 原始パターンパターンはパターンに対するパターンである． この原始パターンパターンはpairパターンにマッチし，このマッチャー節はpairパターンに対するパターンマッチの方法を定義している． pairのように，原始パターンパターン中にあらわれるパターンコンストラクタは，原始パターンパターンコンストラクタ（primitive pattern-pattern constructor）と呼ばれる． pairパターンの引数としてあらわれている$はパターン・ホール（pattern hole）と呼ばれる原始パターンパターンの構成要素で，任意のパターンがマッチする． パターン・ホールにマッチしたパターンは，ネクスト・パターン（next pattern）と呼ばれる． 原始パターンパターンのパターンマッチは，一般の関数型プログラミング言語の代数的データ型に対するパターンマッチとほぼ同じようにおこなわれる． 次に，このマッチャー節のネクスト・マッチャー式は，(integer, integer)である． これは，上記のパターン・ホールに束縛された2つのパターン（pairパターンの引数）がそれぞれintegerマッチャーを使って再帰的にパターンマッチされることを表現している． このマッチャー節は，1つの原始マッチ節（3行目）をとる． 原始データパターンは，ターゲットとパターンマッチされる． 原始データパターンのパターンマッチも，一般の関数型プログラミング言語の代数的データ型に対するパターンマッチとほぼ同じようにおこなわれる． 原始マッチ節のボディは，ターゲットの分解結果を返す． (x, y)と(y, x)はネクスト・ターゲット（next target）と呼ばれ，ネクスト・パターンとネクスト・マッチャーを使って再帰的にパターンマッチされる．

2つ目のマッチャー節（4-5行目）の原始パターンパターンは，パターン・ホールである． パターン・ホールは任意のパターンにマッチするため，1つ目のマッチャー節でマッチしなかったパターンはすべて2つ目のマッチ節で処理される． 1つ目のマッチャー節でマッチしないunorderedIntegerPairに対するパターンは，ワイルドカードかパターン変数のみであるので，このマッチャー節はこれらのパターンを処理する． このマッチャー節は，パターンとターゲットを変えず，ただマッチャーをsomethingに変換するだけである． パターンとターゲットはsomethingを使ってパターンマッチされる． somethingは唯一の組み込みマッチャーであり，以下の3種類のパターンを処理する．

値パターンをsomethingが直接処理するようになったのは，静的型付けの導入にともなう設計変更である（詳しくは後述の6.3節を参照）．

以下のunorderedPairのように，ペアの要素のデータ型に対するマッチャーを受け取るunordered pairに対するマッチャーを定義することができる．

matchAll (1, 2) as unorderedPair integer with
| pair $x $y -> (x, y)
-- [(1,2),(2,1)]

そのためには，まずinductive pattern宣言を型パラメータを使った汎用的な形に変更する．

inductive pattern {a} (a, a) :=
  | pair a a

そして，unorderedPairをマッチャーを引数にとってマッチャーを返す関数として定義すればよい． pairパターンに対するマッチャー節のネクスト・マッチャー式でunorderedPairの引数であるmを指定している． 型注釈により、型パラメータ{a}と引数のマッチャー(m: Matcher a)を受け取り、ペア型(a, a)に対するマッチャーを返すことを示している．

def unorderedPair {a} (m: Matcher a) : Matcher (a, a) := matcher
  | pair $ $ as (m, m) with
    | ($x, $y) -> [(x, y), (y, x)]
  | $ as something with
    | $tgt -> [tgt]

6.3eqマッチャーの定義

eqマッチャーもmatcher式でユーザーが定義することができる． eqマッチャーは値パターンとワイルドカード・パターン変数のみを処理するため，特別なパターンコンストラクタを持たない． したがって，eqマッチャー自体にはinductive pattern宣言は不要である． 型注釈により，型制約{Eq a}を持つ型パラメータaに対するマッチャーであることを示している．

def eq {Eq a} : Matcher a := matcher
  | #$val as () with
    | $tgt -> if val == tgt then [()] else []
  | $ as something with
    | $tgt -> [tgt]

eqマッチャーの1つ目のマッチャー節（2-3行目）は値パターンに対するマッチャー節である． #$valは値パターンにマッチする原始パターンパターンである． このような原始パターンパターンは原始値パターン（primitive value pattern）と呼ばれる． 変数valには値パターンの中身が束縛される． このマッチャー節の原始パターンパターンは，パターン・ホールを含んでいないため，ネクスト・マッチャー式は空タプルである． 原始マッチ節で，値パターンの中身とターゲットの値が等しいかどうかチェックしている．

somethingとeqの違い．

somethingは値パターンを組み込みの構造的同値判定で処理するのに対し，eqはEq型クラスのメソッドであるユーザ定義の==演算子を使って比較する． この2つの使い分けは，マッチャーを引数にとるマッチャー（マッチャーパラメータ化マッチャー）の設計と深く関わっている．

たとえば，multisetのような引数マッチャーmを受け取るマッチャーで値パターンを処理するとき，再帰的な比較の基底ケースをどのマッチャーに委ねるかが問題になる． もしsomethingが値パターンを処理できないとすると，eqマッチャーに委ねるしかなく，eqはEq型クラス制約を必要とするため，multisetの型が

multiset : {Eq a} => Matcher a -> Matcher [a]

のようにEq制約を必要とするものになってしまう． しかしmultisetの多くの用途は値パターンを使わないため，この制約は過度に制限的である．

この問題を解決するために，somethingに組み込みの構造的同値判定による値パターン処理を組み込んだ． これにより，マッチャーパラメータ化マッチャーは，型クラス制約を課すことなくsomethingを基底ケースとして使え，

multiset : Matcher a -> Matcher [a]

という制約のない型を持つことができる． 一方，ユーザ定義の等値比較（==）を使いたい場合には，明示的にeqマッチャーを指定することで対応できる．

原始パターンパターンは，ここまでにでてきた3つの構成要素であるパターン・ホール，原始パターンパターンコンストラクタの適用，原始値パターンと，原始ワイルドカードからなる．

`primitive pattern-pattern` ::= $ | c `primitive pattern-pattern`* | #$`ID` | _

原始ワイルドカードについては，6.6節で用例を紹介する．

原始データパターンは，ワイルドカード，パターン変数，原始データパターンコンストラクタの適用からなる．

`primitive data pattern` ::= _ | $`ID` | C `primitive data pattern`*

6.4multisetマッチャーの定義

本節は，multisetマッチャーの定義を解説する． multisetマッチャーは，6.1節で示したリスト型[a]のinductive pattern宣言で宣言されたパターンコンストラクタ（[]，::，++）を処理するマッチャーである． 型注釈により、型パラメータ{a}と引数のマッチャー(m: Matcher a)を受け取り、リスト型[a]に対するマッチャーを返すことを示している．

def multiset {a} (m: Matcher a) : Matcher [a] := matcher
  | [] as () with
    | $tgt -> match tgt as (mutiset m) with
                | [] -> [()]
                | _ -> []
  | $ :: $ as (m, multiset m) with
    | $tgt -> matchAll tgt as list m with
                | $hs ++ $x :: $ts -> (x, hs ++ ts)
  | #$val as () with
    | $tgt -> match (val, tgt) as (list m, multiset m) with
                | ([], []) -> [()]
                | ($x :: $xs, #x :: #xs) -> [()]
                | (_, _) -> []
  | $ as something with
    | $tgt -> [tgt]

1つ目と4つ目のマッチャー節はほぼ自明であるので，2つ目と3つ目のマッチャー節をみていく．

2つ目のマッチャー節（6-8行目）をみていこう． 原始プリミティブパターンは$ :: $で，ネクスト・マッチャー式は(a, multiset a)である． aはmultisetの引数のマッチャーである． ネクスト・ターゲットは，matchAll式を使って定義されている． このmatchAll式は，ターゲットが[1,2,3]である場合，[(1,[2,3]),(2,[1,3]),(3,[1,2])]を返す． このリストに含まれるそれぞれのネクスト・ターゲットは，ネクスト・パターンとネクスト・マッチャーを使って再帰的にパターンマッチされる． たとえば，ネクスト・ターゲット1と[2,3]は，ネクスト・マッチャーaとmultiset aを使って，コンス・パターンの第1引数と第2引数のパターンとパターンマッチされる．

3つ目のマッチ節をみていこう． このマッチャー節の原始パターンパターンは，原始値パターン#$valである． このマッチャー節は，値パターンを処理する． このマッチャー節は，値パターンの中身（val）とターゲット（tgt）が等しいかどうかくらべる． このmatch式の1つ目と3つ目のマッチ節は自明であるので説明を省略する． 2つ目のマッチ節のパターンは，valの先頭の要素をtgtから取り出す． そして，valとtgtから同じ要素を1つ抜いたコレクションを$xsと#xsというパターンを使って再帰的にパターンマッチしている． #xsのパターンマッチに，このマッチャー節自身が再帰的に呼び出されるが，コレクションの長さが1つずつ短くなっていくため，最終的に1つ目か3つ目のマッチ節どちらかにいきつく．

6.5soretedListマッチャーの定義

二重にネストしたジョイン・コンス・パターンを使って\((p,p+6)\)という形の素数のペアを列挙するプログラムは，後方の素数のペアになるほど列挙に時間がかかるようになる． その理由は，二重にネストしたジョイン・コンス・パターンは，すべての素数の組み合わせを検査するためである． たとえば，このパターンは，\((3,5)\)，\((3,7)\)，\((3,11)\)，\((3,13)\)，\((3, 17)\)，\((3,19)\)のような素数のペアすべてを検査する． しかし，\((3,11)\)以降の素数のペア，差が\(6\)より大きくなる最初の素数のペア，以降のペアについては，\((p,p+6)\)であるか検査する必要はない．

take 10 (matchAll primes as sortedList integer with
         | _ ++ $p :: (_ ++  #(p + 6) :: _) -> (p, p + 6))
-- [(5,11),(7,13),(11,17),(13,19),(17,23),(23,29),(31,37),(37,43),(41,47),(47,53)]

ソート済みリストに特化したマッチャーを使うことにより，この不必要な探索は避けることができる． 通常のlistマッチャーに，$ ++ #$px : $を原始パターンパターンにもつマッチャー節を追加すれば，ソート済みリストに特化したマッチャーをつくることができる． このマッチャー節が，\((p,p+6)\)という形の素数のペアにマッチする二重にネストしたジョイン・コンス・パターンの計算量を\(O(n^2)\)から\(O(n)\)に減らす． 型注釈により、型制約{Ord a}を持つ型パラメータaとマッチャー引数(m: Matcher a)を受け取り、ソート済みリスト型[a]に対するマッチャーを返すことを示している．

def sortedList {Ord a} (m: Matcher a) : Matcher [a] := matcher
  | $ ++ #$px :: $ as (sortedList m, sortedList m) with
    | \$tgt -> matchAll tgt as list m with
               | loop $i (1, $n)
                   ((?(\x -> x < px) & $h_i) :: ...)
                   (#px :: $ts)
                 -> (map (\i -> h_i) [1..n], ts)
  ...

このようにネストしたパターンに対して直接パターンマッチのアルゴリズムを定義することによる最適化のことを，パターン・フュージョン（pattern fusion）と呼ぶ．

6.6原始ワイルドカードによる最適化

パターンがワイルドカードを含む場合，ワイルドカードにマッチするターゲットの計算を省くことにより，パターンマッチの処理を高速化できる． 原始パターンパターン中で，原始ワイルドカードを使うことにより，Egisonではこの最適化をおこなえる． 本節は，6.4節で紹介したmultisetマッチャーについて，そのような最適化を紹介する． このような最適化のことを，ワイルドカード最適化（wildcard optimization）と呼ぶ．

本節で紹介する最適化の対象は，以下のようなコンス・パターンの第二引数がワイルドカードである場合である． この場合，対象のコレクションから要素を1つ除いた残りのコレクションを計算する必要はない． 原始ワイルドカードを使うことにより，この計算を省くようにmultisetマッチャーに記述することができる．

matchAll [1, 2, 3, 4, 5] as multiset eq with
| $x :: _ -> x
-- [1, 2, 3, 4, 5]

このような最適化は，以下の2-3行目のマッチャー節を6.4節のmultisetマッチャーの定義に追加すればできる． このマッチャー節の原始パターンパターンで原始ワイルドカードが使われている． パターン・ホールはコンス・パターンの第一引数だけであるので，ネクスト・マッチャーはmだけになり，ネクスト・ターゲットはtgtのそれぞれの要素であるために，tgtをそのまま返すようになっている．

def multiset {a} (m: Matcher a) : Matcher [a] := matcher
  | $ :: _ as m with
    | $tgt -> tgt
  | $ :: $ as (m, multiset m) with
    | $tgt -> matchAll tgt as list m with
              | $hs ++ $x :: $ts -> (x, hs ++ ts)
  ...

6.5節のsortedListマッチャーも同様の最適化ができる． 下記の2-7行目のマッチャー節は，ジョイン・パターンの第一引数を計算することを省略する役割を果たす．

def sortedList {Ord a} (m: Matcher a) : Matcher [a] := matcher
  | _ ++ #$px :: $ as sortedList m
    | \tgt -> matchAll tgt as list m with
              | loop $i (1, _)
                  (?(\x -> x < px) :: ...)
                  (#px :: $ts)
                -> ts
  | $ ++ #$px :: $ as (sortedList m, sortedList m)
    | \tgt -> matchAll tgt as list m with
              | loop $i (1, $n)
                  ((?(\x -> x < px) & $h_i) :: ...)
                  (#px :: $ts)
                -> (map (\i -> h_i) [1..n], ts)
  ...

6.7assocMultisetマッチャー

Egisonには，多重集合に対するマッチャーとして，assocMultisetが用意されている． 本節はその使い方と定義を紹介する．

多重集合は，要素のその個数の連想リストとして表現できる． assocMultisetマッチャーは，このように連想リストとして表現された多重集合に対するマッチャーである． たとえば，以下のプログラムは\(1\)を\(4\)個，\(2\)を\(3\)個，\(3\)を\(1\)個もつ多重集合に対してパターンマッチをしている． ターゲットの多重集合に\(3\)個以上現れる要素を取り出すパターンが表現されている．

matchAll [(1, 4), (2, 3), (3, 1)] as assocMultiset eq with
  | $x ^ #3 :: $rs -> (x, rs)
-- [(1, [(1, 1), (2, 3), (3, 2)]), (2, [(1, 4), (3, 2)])]

6.8マッチャーとパターンの型

ここまでのマッチャー定義には，Matcher (Integer, Integer)のような型注釈が現れていた． 本節からは，パターンマッチが型システムでどのように検査されるかを解説する．

Egisonの型システムでは，マッチャーとパターンにそれぞれ型が付く． Matcher aはa型の値を対象とするマッチャーの型であり，Pattern aはa型の値にマッチするパターンの型である． マッチャーは第一級の値なので，multisetのようにマッチャーを引数にとってマッチャーを返す関数も型をもつ． たとえば，コレクションの基本マッチャーは以下の型をもつ．

something : Matcher a
eq        : {Eq a} => Matcher a
list      : MatcherSlot a a -> Matcher [a]
multiset  : MatcherSlot a a -> Matcher [a]
set       : MatcherSlot a a -> Matcher [a]

引数マッチャーの位置には，Matcherではなくスロット型MatcherSlot a bが使われる． スロット型は2つの型をとる． 第一成分aはその位置で使われるパターンが要求する分解（構造）の型， 第二成分bはその位置のターゲット（分解される値）の型である． listやmultisetの要素位置のように両者が一致する場合は，「おおよそMatcher aを受け取る」と読んでよい． スロット型が分解の型とターゲットの型を別々にもつのは，そこに渡されるマッチャーがその位置のパターンを実際に分解できるかを， 渡された場所ごとに検査するためである．この検査については6.10節で改めて扱う．

この型の一覧には設計上の要点がひとつ隠れている． listやmultisetの型にEq制約が付いていないことである． 値パターン（#5など）の照合はsomethingのレベルで構造的な等価性により処理されるため， コレクションのマッチャー自体は要素の等価性を要求しない． そのおかげで，等価性が定義されていない型（たとえばシンボリックな数式や抽象構文木）に対しても multisetなどのマッチャーをそのまま使うことができる． 第2章2.10節のintersectのようにeqマッチャーを明示的に使うのは， Eq型クラスのインスタンスによるカスタムの等価性で照合したい場合である．

6.9パターンの型検査

パターンには，どのマッチャーで使われるかと独立に型が付く（マッチャー多相）． たとえば$x :: $xsはPattern [a]という型をもち， だからこそ同じパターンをlist integerでもmultiset integerでも使うことができる．

値パターンの型検査には束縛の順序が関わる． パターンは左から右へ向かって束縛を増やしながら検査され， 値パターン#eの式eは，それまでに束縛されたパターン変数を参照できる．

matchAll [1, 2, 3, 1] as multiset integer with
  | $x :: #x :: _ -> x
-- [1, 1]

このパターンは「ある要素xと，それと同じ値の要素がもうひとつある」ことを表す非線形パターンであり， #xは直前の$xの束縛（Integer型）の下で型検査される．

型検査は，動的な処理系では黙って失敗するだけだった誤りを静的に検出する． まず，値パターンの中の式の型の誤りは，そのまま型エラーとして報告される．

matchAll [1, 2, 3] as multiset integer with
  | $x :: #(x ++ [1]) :: _ -> x
-- Type error: (++) expects [Integer] but x is Integer

つぎに，値パターンを置く位置の誤りも検出される．

matchAll [1, 2, 3] as multiset integer with
  | $x :: #x -> x
-- Type error: the second argument of :: requires
--   Pattern [Integer], but #x has type Pattern Integer

プログラマの意図は「xが残りにも現れる」だったはずだが，::の第二引数はリスト全体にマッチする位置である． 正しくは$x :: #x :: _と書く． 動的な処理系では，このパターンは何も報告せずにマッチに失敗するだけであった． 最後に，束縛より左で変数を参照する誤りは，未束縛変数の警告として検出される （strictモードでは型エラーになる）．

matchAll [1, 2, 3] as multiset integer with
  | #x :: $x :: _ -> x
-- Warning: unbound variable x
--   (#x refers to x left of its binding $x)

6.10match式の型検査

match式・matchAll式では，ターゲット・マッチャー・パターン・ボディの型がすべて整合しなければならない． ターゲットの型がaなら，マッチャーはMatcher a，各マッチ節のパターンはPattern aであり， すべてのマッチ節のボディの型は一致する必要がある．

たとえば，コレクション用のパターンコンストラクタを整数のマッチャーと組み合わせると型エラーになる．

matchAll 5 as integer with
  | $x :: _ -> x
-- Type error: :: targets collections [a], but the
--   target and the matcher are for Integer

ボディの型の不一致も検出される． たとえば第2章2.9節のtwinの例で ボディを[n, ns]と書くと，Integerと[Integer]が混在するリストになるため型エラーになる （タプル(n, ns)を使う）．

さらに，パターンが要求する分解をマッチャーが提供できるかも検査される（適合性検査）． 変数パターンと値パターンしか使わないパターンは分解を要求しないので，任意の型でsomethingと組み合わせられる． 一方，::のようなパターンコンストラクタを使うパターンには，それを分解できるマッチャーが必要である． somethingは任意の値に単一のマッチをするだけで分解の手段をもたないため， コンスパターンと組み合わせると型エラーになる．

matchAll [1, 2, 3] as something with
  | $x :: $xs -> (x, xs)
-- Type error: something (Matcher a) does not fit
--   MatcherSlot [_] [Integer]
--   (something offers no way to decompose a list)

これが，マッチャーを受け取る位置をMatcherではなくスロット型で型付けする理由である． ここでは，コンスパターンがスロットの分解成分に[_]（リストの分解）を要求するのに対し， somethingはそれを提供できない． 素朴にsomethingをMatcher [Integer]とみなす型システムでは，この式は型検査を通ってしまい， 実行時にsomethingがコンスを分解できずに行き詰まる． Egisonの型システムは，マッチャーが渡された場所ごとに分解の適合を検査するので，この誤りを静的に弾く． この検査はパターンの構造だけから計算されるため，マッチャーを実行しなくても誤った組み合わせが静的に弾かれる．

6.11マッチャー定義の整合性検査

マッチャー定義そのものも型検査の対象である． 各マッチャー節について，原始パターンパターン・ネクスト・マッチャー式・原始データパターンの型の整合が検査されるのに加えて， 原始データパターンのアームの網羅性が要求される． あるマッチャー節の原始パターンパターンがパターンにマッチすると， ターゲットの照合はその節のアームだけで行われ，どのアームにもマッチしなければ実行時エラーになる． そのため，アームの集合が網羅的でないマッチャー定義は型エラーとして拒否される．

def bad {a} (m : MatcherSlot a a) : Matcher [a] :=
  matcher
    | $ :: $ as (m, bad m) with
      | $x :: $xs -> [(x, xs)]    -- missing final | _ -> []
    | $ as something with
      | $tgt -> [tgt]
-- Type error: the data-pattern arms of matcher
--   clause :: $ $ are non-exhaustive

コンス・パターンの節のアームが$x :: $xsだけだと，空リストがターゲットに来たときにどのアームにもマッチせず， 実行時に失敗してしまう． 末尾に| _ -> []を追加すれば「分解できないときはマッチ失敗（候補なし）」という意味になり，網羅的になる． 網羅的と認められるアームの形は，（1）末尾のワイルドカード・アーム，（2）[]と::のペア（コレクションに対して完全）， （3）反駁不能な単一アーム（$tgtなど）である．

6.12パターン関数の型

第2章2.9節で導入したパターン関数にも型が付く．

def pattern twin {a} (pat1: a) (pat2: [a]) : [a] :=
  (~pat1 & $x) :: #x :: ~pat2

この定義において，仮引数の型注釈(pat1: a)は「pat1はa型の値にマッチするパターン」を表し， 返り値位置の: [a]は「適用結果は[a]型の値にマッチするパターン」を表す． つまりtwinの型はおおよそPattern a -> Pattern [a] -> Pattern [a]と読める． 適用時には引数パターンの型が検査される．

matchAll [1, 2] as multiset integer with
  | twin ($y :: _) _ -> y
-- Type error: the first argument requires
--   Pattern Integer, but $y :: _ is Pattern [Integer]

パターン関数の適用は，適合性検査（6.10節）では本体のパターンの骨格として扱われる． twinの本体はコンス・パターンの入れ子なので，twinを使うマッチ式にはコンスを分解できるマッチャー （listやmultiset）が必要である． 逆に，本体が仮引数そのものであるようなパターン関数は構造を課さないため，引数パターンの要求だけが伝播する． このように，パターン関数を経由しても「そのパターンにどんなマッチャーが必要か」が静的に追跡される．

この本を別の言語で読む: English, 日本語