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 に関連して、2つのデータコンストラクタ (や値コンストラクタ) list_nil と list_cons があります。 これらは次の型で宣言されています:
型 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))
依存データ型を用いたプログラミングの例として、次のコードは与えられたリストの長さを算出する関数テンプレートを実装しています:
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]
与えられた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 もまた存在します:
例として、 次の関数テンプレート 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 は明らかに末尾再帰であり、停止することは検査済みです。
プログラマは list と option に慣れ親しんだ後 list0 と option0 を使う動機はほとんどないでしょう。 内部では、list と list0 の値は全く同じ表現を持ちます。 さらに list と list0 の値を相互変換するキャスト関数が ATS にはあります。 option と option0 の値についても同様です。