ATSプログラミング入門:
PrevNext

Chapter 9. 依存型入門

Table of Contents
仕様に対する表現力の強化
型検査中での制約解決
例: 文字列処理
例: 配列の二分探索
再帰関数の停止性検査
例: 依存型を使ったデバッグ

この本でこれまで見てきた型は、しばしばプログラミングの不変条件を正確に表現していませんでした。 例えば型 int を整数 0 と 1 の両方に割り当てると、型のレベルでは 0 と 1 を単純に見分けることができません。 これは型検査の範囲では 0 と 1 が交換可能であることを意味しています。 別の言い方をすると、もし 0 であるべきところを 1 とミスタイプして、型検査中に捕捉すべきプログラムのエラーが起きても、型検査時に予測できません。 もし、実際の使用に耐える表現力豊かな型ベースの仕様記述言語を作ろうとしたなら、型におけるこの種の不正確さは不自由な制限になりえます。

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

仕様に対する表現力の強化

ATS の型システムに依存型を導入する主要な目的は、プログラムの不変条件をより正確に捕捉できるように、型の表現力をより強化することです。 一般的には、依存型とは式の値に依存した型のことです。 例えば、bool は与えられたブール値 b に適用されると型 bool(b) を作るような ATS の型コンストラクタです。 この型は値 b のブール式にのみ割り当てることができ、これはしばしばシグルトン型と呼ばれます。 つまりきっちり1つの値しか持たない型を意味します。 明らかに、bool(b) の意味はブール値 b に依存しています。 同様に、int は ATS の型コンストラクタで、与えられた整数 i に適用されて型 int(i) を作ります。 また、この型は値 i の整数式にのみ割り当てることができるようなシングルトン型です。 bool と int は両方ともオーバーロードされて (依存型でない) 型を参照していることに注意してください。 ここでは依存型の他の例を徐々に紹介します。 特に、依存データ型を宣言する柔軟な手法を紹介します。

ATS の静的な部分は単純型付き言語で、(動的な項の型 (type) と) 混乱する可能性を回避するために、この言語の型は 種 (sort) と呼ばれます。 次に挙げる4つの種が一般的に使用されます:

種 bool と int は述語種 (predicative sorts) に、 種 type と t@ype は非述語種 (impredicative sorts) に分類されます。 ボックス化型は種 type の静的な項です。 アンボックス化型は種 t@ype の静的な項です。 型としての bool と int は種 t@ype の静的な項です。 型コンストラクタとしての bool と int はそれぞれ種 (bool -> t@ype) と (int -> t@ype) の静的な項です。 型コンストラクタ list0 もまた種 (t@ype -> type) であることに注意してください。 これは list0 はアンボックス化型に適用するとボックス化型を作ることを示しています。 種 bool と int の静的な項をコンストラクトするために、ATS にはビルトインの静的な関数が多数用意されています。 次にこのような関数のいくつかを割り当てられた種と一緒に挙げてみます:

種と1つ以上の述語を結合して、サブセット種を定義できます。 例えば、次のサブセット種が basics_pre.sats ファイルで定義されていて、ATSコンパイラが自動的にロードします: 

sortdef nat = {a: int | a >= 0} // for natural numbers
sortdef pos = {a: int | a >= 1}  // for positive numbers
sortdef neg = {a: int | a <= ~1}  // for negative numbers

sortdef nat1 = {a: nat | a < 1} // for 0
sortdef nat2 = {a: nat | a < 2} // for 0, 1
sortdef nat3 = {a: nat | a < 3} // for 0, 1, 2
sortdef nat4 = {a: nat | a < 4} // for 0, 1, 2, 3

セミコロン記号 (;) を使って述語群を結合することで、それらの並べることができることに注意してください: 

sortdef nat2 = {a: int | 0 <= a; a < 2} // for 0, 1
sortdef nat3 = {a: int | 0 <= a; a < 3} // for 0, 1, 2
sortdef sgn = { i:int | ~1 <= i; i <= 1 } // for ~1, 0, 1

次のようにサブセット種 nat2 と nat3 を定義することも可能です: 

sortdef nat2 = {a: int | a == 0 || a == 1} // for 0, 1
sortdef nat3 = {a: int | 0 <= a && a <= 2} // for 0, 1, 2

ここのとき || と && はそれぞれ論理和と論理積を表わしています。

依存型の表現力を解き放つために、静的な値の上に全称量化 (universal quantification) と存在量化 (existential quantification) を採用しましょう。 例えば、ATSの型 Int は次のように定義されています: 

typedef Int = [a:int] int (a) // for unspecified integers

ここでは、構文 [a:int] は、種 int の静的な変数 a の上の存在量化を意味しています。 これは本質的に、型 Int のそれぞれの値に対して、型 int(I) の値になるような整数 I が存在することを意味します。 したがって、型 int が与えられるどのような値にも型 Int を与えることができます。 Int のような型はしばしば存在量化型 (existentially quantified type) と呼ばれます。 別の例として、ATSの型 Nat は次のように定義されます: 

typedef Nat = [a:int | a >= 0] int (a) // for natural numbers

ここでは、構文 [a:int | a >= 0] は、不変条件 a >= 0 を満たすような種 int の静的な変数 a の上の存在量化を意味しています。 したがって、型 Nat のそれぞれの値には I >= 0 を満たす整数 I を使った型 int(I) を割り当てることができます。 int(I) がシングルトン型として与えられると、その値は I に等しく、自然数になります。 つまり型 Nat は自然数を意味することになります。 Nat はまた次のようにも定義できます: 

typedef Nat = [a:nat] int (a) // for natural numbers

ここでは、構文 [a:nat] は単なる構文糖衣で、自動的に [a:int | a >= 0] に展開されます。

現時点で型の表現力はすでに強化されています。 例えば、型 (int) -> int は整数を自然数に写像する関数に割り当てることができました (例: 与えられた整数の絶対値を計算する関数)。 しかし、そのような関数には型 (Int) -> Nat を割り当てた方がより良いでしょう。 その方がより明確になります。 型レベルで関数の返値とその引数を関連付けるためには、全称量化が必要になります。 例えば、次の全称量化型は、引数として渡された整数の次の数を返すような関数を表わしています: 

{i:int} int (i) -> int (i+1)

構文 {i:int} は種 int の静的な変数 i の上の全称量化を意味しています。 この全称量化のスコープは、それに続く関数型の中です。 読者は、この型の唯一の関数は整数の後者関数 (successor function) であり、この関数型もまたシングルトン型であると考えるかもしれません。 実際には、この型を与えられる部分関数が無数に存在します。 自然数の後者関数に、次のような型を使うことができます: 

{i:int | i >= 0} int (i) -> int (i+1)

構文 {i:int | i >= 0} は不変条件 i >= 0 を満たすような種 int の静的な変数 i の上の全称量化を意味しています。 この型はまた次のように書くこともできます: 

{i:nat} int (i) -> int (i+1)

構文 {i:nat} は自動的に {i:int | i >= 0} に展開されます。 整数に一般的に使われるいくつかのインターフェイスを次に挙げます: 

fun g1int_neg {i:int} (int i): int (~i) // negation
fun g1int_add {i,j:int} (int i, int j): int (i+j) // addition
fun g1int_sub {i,j:int} (int i, int j): int (i-j) // subtraction
fun g1int_mul {i,j:int} (int i, int j): int (i*j) // multiplication
fun g1int_div {i,j:int} (int i, int j): int (i/j) // division

fun g1int_lt {i,j:int} (int i, int j): bool (i < j) // less-than
fun g1int_lte {i,j:int} (int i, int j): bool (i <= j) // less-than-or-equal-to
fun g1int_gt {i,j:int} (int i, int j): bool (i > j) // greater-than
fun g1int_gte {i,j:int} (int i, int j): bool (i >= j) // greater-than-or-equal-to
fun g1int_eq {i,j:int} (int i, int j): bool (i == j) // equal-to
fun g1int_neq {i,j:int} (int i, int j): bool (i != j) // not-equal-to

これらのインターフェイスは全て integer.sats ファイルで宣言されていて、ATS コンパイラが自動的にロードします。 ここで挙げた関数群は全てそれらの標準名で参照可能であることに注意してください: ほとんどの場合、 ~ は g1int_neg, + は g1int_add, - は g1int_sub, * は g1int_mul, / は g1int_div, < は g1int_lt, <= は g1int_lte, > は g1int_gt, >= は g1int_gte, = は g1int_eq, != は g1int_neq, <> は g1int_neq を参照しています。

この興味深い質問を持ち出すには今が適切な時でしょう: 階乗関数の依存型インターフェイスはどのようになるでしょうか？ 上記の例を見た後では、次の行のように考えるのが自然でしょう: 

fun g1int_fact {i:nat} (i: int i): int (fact (i))

このとき、fact は階乗関数の静的なバージョンです。 この答には大きな問題があります。 fact のような静的な関数を ATS では定義できないのです。 ATS の静的な部分は単純型付き言語であり、静的な項のコンストラクトにおいてどのような再帰的な意味も許されていません。 このデザインを採用しているのは、主に現実的なアルゴリズムをベースに静的な項の等価性を決定できるように保証するためです。 本質的に、依存型を伴う型検査は、静的な項における等価性 (とビルトインの述語) の集合の検査に変化します。 そのようなデザインは、依存型を使った実際のプログラミングをサポートするためにきわめて重要です。 関数の定義に正確に一致する階乗関数にインターフェイスを割り当てるためには、ATS に定理証明を使ったプログラミングを採用する必要があります。 このトピックは後の章で取り上げます。

PrevHomeNext
依存型を使ったプログラミングUp型検査中での制約解決