ATSプログラミング入門:
PrevChapter 10. データ型の改良Next

パターンマッチの連続性

ATS では、パターンマッチは実行時において連続して評価されます。 別の言い方をすると、節が選択されるのは与えられた値がその節に関連するパターンガードにマッチし、しかも値がその前にあるどの節のパターンにもマッチしない場合にだけです。 当然、list_zipwith 次の実装も型検査できると期待するでしょう: 

fun{
a,b:t@ype
}{c:t@ype
} list_zipwith
  {n:nat}
(
  xs: list(a, n)
, ys: list(b, n)
, f: (a, b) -<cloref1> c
) : list(c, n) = (
//
case+ (xs, ys) of
| (
    list_cons(x, xs)
  , list_cons(y, ys)) =>
  (
    list_cons(f(x, y), list_zipwith<a,b><c>(xs, ys, f))
  )
| (_, _) => list_nil((*void*))
//
) (* end of [list_zipwith] *)

けれども、この場合は型検査に失敗します。 ATS では、節の型検査は(連続的と言うよりむしろ)非決定的です。 この例では、2番目の節が型検査に失敗します。 与えられたペア (xs, ys) が最初の節のパターンガードへのマッチに失敗することが仮定されていないからです。 次のように少し修正することで2番目の節は型検査を通ります: 

  | (_, _) =>> list_nil ()

記号 => の代わりに =>> を使うと、その前のいずれの節のパターンガードにもマッチしなかったという連続的な仮定において、この節が型検査されるべきであると、型検査器に指示します。 したがって、修正された2番目の節が型検査されると、パターン (_, _) にマッチするペア (xs, ys) は次の3つのパターンのにマッチするはずだということが仮定できます:

同じ長さの xs と ys が与えられた時、 型検査器は (xs, ys) は最初の2パターンにマッチしないとたやすく推論できます。 これら2パターンが除外されたら、2番目の節が次のように書かれていることになり、 型検査は本質的に終わったということになります: 

  | (list_nil (), list_nil ()) => list_nil ()

なぜ節の型検査がデフォルトで連続的に行なわれないのか気にするかもしれません。 その単純な理由は、全体に適用すると型検査の効率に大きなマイナスの影響があるからです。 したがって、特定の節の型検査に連続的な仮定を時々使うための明確な手段をプログラマに提供するのは、妥当なデザインなのです。

PrevHomeNext
例: リストのマージソート (再)Up例: 関数的な赤黒木