こわくない Idris (3)

ハロー、依存型プログラミングの世界 (3)

依存ペア

依存ペア dependent pair とは、ある値と、その値に依存した型を持つ値のペアのことだ。

data Exists : (a : Type) -> (P : a -> Type) -> Type where
    Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

Ex_introによって作られたペアは、aという型の値xと、xに依存した P x という型を持った値を保持している。なぜこのデータ型の型コンストラクタがExistsという名前なのかと言えば、Exists A Pという型が という命題に対応するからだ。型と命題の対応関係については後に述べる。

REPLでExistsを使ってみると、たとえばこうなる。

Idris> the (Exists Nat (\n => Vect n Integer)) (Ex_intro 4 [1, 2, 3, 4])
(4 ** [1,2,3,4]) : (n ** Vect n Integer)

\n => Vect n Integer というのは、単なるラムダ記法である。型の表現に普通の函数を用いることができることが分かる。この部分は flip Vect Integer と表現することもできる。

REPLの出力は奇妙な表示になっている。Ex_intro x y のシンタックスシュガーとして (x ** y) という表記が使われている。また、型注釈にも Exists A P のシンタックスシュガーとして (x : A ** P x) という表記があり、さらにその省略形の (x ** P x) が使われる。それぞれの記法を混同しないように注意する必要がある。

シンタックスシュガーを用いた例を示す。

Idris> the (n : Nat ** Vect n Integer) (4 ** [1, 2, 3, 4])
(4 ** [1,2,3,4]) : (n ** Vect n Integer)

依存ペアがどのような場面で使われるかの例として、IdrisのチュートリアルにはVectに対するfilter函数の例が出てくる。

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

省略せずに書けば、filter : {a : Type} -> {n : Nat} -> (a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)となる。
filter函数の返り値の型は結果のベクトルの長さpに依存して変わってしまうので、pと結果のベクトルからなる依存ペアを返すようになっている。依存ペアを使わずに filter : (a -> Bool) -> Vect n a -> Vect p a とすると、これは filter : {a : Type} -> {n : Nat} -> {p : Nat} -> (a -> Bool) -> Vect n a -> Vect p a という意味で、フィルターする前に結果の長さが分かっていることになってしまう。

演習問題

依存ペアの左右の値はそれぞれgetWitnessとgetProofという函数で取り出すことが出来る。それぞれの函数の型を調べなさい。また、次の式をREPLで評価した結果を予想し、確かめなさい。

getWitness (the (n ** Vect n Integer) (_ ** [4, 5, 6]))