網羅的なパターンマッチ

T 型と複数のパターンが与えられた時、どのような T 型の値に対しても必ず一つ以上のパターンがマッチするなら、このパターン群を使った T 型の値のパターンマッチは網羅的です。 exp0 が型 T で、ケース式 (case exp0 of clseq) が与えらた時、clseq 中のマッチ節のガードに対して型 T の値のパターンマッチが網羅的であるなら、このケース式は網羅的なパターンマッチであると呼ばれます。

次のコードは空でない文字リストの最後の文字を見つけるような関数の実装です:

fun
charlst_last
  (cs: charlst): char =
(
  case cs of
  | charlst_cons (c, charlst_nil ()) => c
  | charlst_cons (_, cs1) => charlst_last (cs1)
)
// end of [charlst_last]

関数 charlst_last はまた次のように実装することもできます:

fun
charlst_last
  (cs: charlst): char =
(
  case cs of
  | charlst_cons (c, cs1) =>
    (
      case+ cs1 of
      | charlst_nil () => c | charlst_cons _ => charlst_last (cs1)
    ) // end of [charlst_cons]
) // end of [charlst_last]

たった1つだけマッチ節を持つケース式、つまり [case exp0 of pat => exp] という形のケース式を考えましょう。 するとこのケース式は (let val pat = exp0 in exp end) のように let 式で書くこともできます: 例えば、関数 charlst_last は次のような別の実装をすることができます:

fun
charlst_last
  (cs: charlst): char = let
  val charlst_cons (c, cs1) = cs in case+ cs1 of
  | charlst_nil () => c | charlst_cons _ => charlst_last (cs1)
end // end of [charlst_last]

コンストラクタ charlst_nil と charlst_cons で作られる値が同じ型 charlst を持つ時、関数 charlst_last が空の文字リストに適用されてしまうことを型検査で防止することは不可能です。 これは深刻な制限です。 データをより正確に表現できる依存型を使えば、リストの最後の要素を見つける関数を空でないリストにのみ適用することを、型のレベルで保証できるようになります。