Chapter 10. データ型の改良

Table of Contents
依存データ型
例: リストに対する関数テンプレート (再)
例: リストのマージソート (再)
パターンマッチの連続性
例: 関数的な赤黒木

ATS におけるデータ型のメカニズムは ML から直接輸入しています。 関数型プログラミングにおいてこの機能はお墨付きです。 けれども、これまで見てきたデータ型は値を分類するに十分に正確というわけでもありません。 例えば型 T が与えられた時、型 T の要素から成る空のリストと空でないリストを表わす値は両方とも型 list0(T) です。 したがって、空のリストと空でないリストは型レベルで区別がつきません。 プログラムの不変条件を捕捉する ML スタイルのデータ型の有効性が、この制限によってしばしば減少してしまいます。 ATS では、ML スタイルのデータ型は DML スタイルの依存データ型に改良することができます。 この DML とは ATS の祖先であるプログラミング言語 Dependent ML のことです。 このような改良によって、データ型は値をより正確に分類できます。

この章で紹介するコードと追加のテストコードは オンライン から入手できます。

依存データ型

依存データ型を宣言する構文は非依存データ型を宣言する構文とほとんど同じです。 例えば、ATS の依存データ型 list は次のように宣言されています:

datatype list(t@ype+, int) = | {a:t@ype} list_nil(a, 0) of () // [of ()] is optional | {a:t@ype} {n:nat} list_cons(a, n+1) of (a, list(a, n))

より正確には、list は種 (t@ype, int) -> type の型コンストラクタとして宣言されています。 これは list はアンボックス化型と静的な整数を取りボックス化型を作ることを意味しています。 キーワード t@ype+ は、 list が種 t@ype である最初のパラメータについて共変 (covariant) であることを示しています。 つまり T1 が T2 のサブタイプであるなら、list(T1, I)list(T2, I) のサブタイプであるということになります。 また、宣言された型コンストラクタがパラメータについて反変 (contravariant) であることを示すキーワード t@ype- も存在しますが、実際にはあまり使われません。 また type+type- のようなキーワードも同等に解釈されます。

list に関連して、2つのデータコンストラクタ (や値コンストラクタ) list_nillist_cons があります。 これらは次の型で宣言されています:

list_nil : {a:t@ype} () -> list(a, 0)
list_cons : {a:t@ype}{n:nat} (a, list(a, n)) -> list(a, n+1)

型 T と静的な整数 I が与えられた時、 要素の型が T で長さが I のリストを表現する値は型 list(T, I) です。 ゆえに、型 list_nil は長さ 0 のリストを、 型 list_cons は要素と長さ n のリストに適用すると長さ n+1 のリストを作ることを意味しています。 次のようなより簡潔なスタイルで list を宣言することもできることに注意してください:

datatype list (a:t@ype+, int) = | list_nil(a, 0) of () // [of ()] is optional | {n:nat} list_cons(a, n+1) of (a, list(a, n))

t@ype+ の代わりに a:t@ype+ を使うことで a の上に全称量化を暗黙的に導入します。 この a は宣言された型コンストラクタ list に関連するデータコンストラクタに割り当てられた型です。

依存データ型を用いたプログラミングの例として、次のコードは与えられたリストの長さを算出する関数テンプレートを実装しています:

fun{ a:t@ype } list_length {n:nat} .<n>. // .<n>. is a termination metric (xs: list (a, n)): int (n) = case+ xs of | list_nil () => 0 | list_cons (_, xs1) => 1 + list_length (xs1) // end of [list_length]

関数 list_length の型は自然数 n 長さのリストを取り、整数の値 n を返すことを示しています。 加えて、この関数は停止することが検査されています。 したがって、list_length が与えられたリストの長さを計算する関数を実装していることが保証されています。 list_length の定義に対する型検査がどのように行なわれるのか簡単に説明してみます。 はじめに次の節の型検査を見てみましょう:

  | list_cons (_, xs1) => 1 + list_length (xs1)

私達が検査しなければならないのは、xs 記号 => の左側にあるパターンにマッチすると仮定して、記号 => の右側にある式に型 int(n) を割り当てることができるかどうかです。 自然数 n1 について xs1 の型が list(a, n1) だと仮定してみましょう。 この仮定はパターン list_cons(_, xs1) は型 list(a, n1+1) であることを意味します。 xs がパターン list_cons(_, xs1) にマッチすることから、n=n1+1 は明確です。 list_length(xs1) の型が int(n1) であり、したがって 1 + list_length(xs1) の型が int(1+n1) であることもまた明確です。 n=n1+1 であれば n=1+n1 であるので、 1 + list_length(xs1) には型 int(n) が与えられることになります。 この節の型検査はこのようになりました。 パターン list_nil()xs がマッチする場合、n=0 を仮定できることに注意してください。 この仮定は 0 が型 int(n) であることを示しています。 したがって、次の節が型検査できました:

  | list_nil((*void*)) => 0

与えられた2つの節の型検査がおわれば、それらを含む case 式には型 int(n) を割り当てることができます。 したがって list_length の定義が型検査できました。

上記で定義されている関数 list_length の本体での再帰呼出は末尾呼出ではないため、この関数は (例えば100万個の要素を持つような) 長いリストを扱うことができません。 次のコードは与えられたリストの長さを計算する別の実装です:

fun{ a:t@ype } list_length{n:nat} .<>. (xs: list (a, n)): int (n) = let // loop: {i,j:nat} (list (a, i), int (j)) -> int (i+j) fun loop {i,j:nat} .<i>. // .<i>. is a termination metric (xs: list (a, i), j: int j): int (i+j) = case+ xs of | list_cons (_, xs1) => loop (xs1, j+1) | list_nil () => j // end of [loop] in loop (xs, 0) end // end of [list_length]

このとき list_length は末尾再帰関数 loop を使っています。 そのためどのような長さのリストも一定のスタック量で扱うことができます。 loop の型は、自然数 i と j について loop が長さ i のリストと値 j の整数を取り、値 i+j の整数を返すことを示していることに注意してください。 また loop が停止することは検査済みです。

ATS ではオプション値を成す依存データ型 option もまた存在します:

datatype option(a:t@ype+, bool) = | Some (a, true) of a | None (a, false) of () // end of [option]

例として、 次の関数テンプレート list_last は与えられたリストの最後の要素を探します:

fun{ a:t@ype } list_last {n:nat} .<>. ( xs: list (a, n) ) : option (a, n > 0) = let // fun loop {n:pos} .<n>. ( xs: list (a, n) ) : a = let val+ list_cons (_, xs1) = xs in case+ xs1 of | list_cons _ => loop (xs1) | list_nil () => let val+ list_cons (x, _) = xs in x end // end of [list_nil] end // end of [loop] // in case+ xs of | list_cons _ => Some (loop (xs)) | list_nil () => None () end // end of [list_last]

内部の関数 loop は明らかに末尾再帰であり、停止することは検査済みです。

プログラマは listoption に慣れ親しんだ後 list0option0 を使う動機はほとんどないでしょう。 内部では、listlist0 の値は全く同じ表現を持ちます。 さらに listlist0 の値を相互変換するキャスト関数が ATS にはあります。 optionoption0 の値についても同様です。