こわくない Idris (5)

プログラミング

表明から証明へ (2)

型と命題

カリー゠ハワード同型対応により、プログラムと証明が対応すると述べた。実際にはどのように対応しているのだろうか? 実は、恒真である命題は、空でない（その型である値を持つ）型に対応しているのだ。
型と命題の対応関係を見てみよう。

型 命題
(x : A) -> P x \forall x \in A (P(x))
(x : A ** P x) \exists x \in A (P(x))
Not P \neg P
(P, Q) P \wedge Q
Either P Q P \vee Q
P -> Q P \rightarrow Q

ここで、NotはBuiltins.idrで次のように定義されている。

Not : Type -> Type
Not a = a -> _|_

_|_ という奇妙な型は、HaskellのData.Void型と同じで、その型である値を持たない型だ。_|_を証明として読むと、矛盾があるという意味に読むことができる。

=

重要なデータ型に(=)がある。これはビルトインのデータ型だが、チュートリアルによれば概念的には次のように表せるものだ。

data (=) : a -> b -> Type where
  refl : x = x

x = y という型は、x と y が同じものである場合にだけ、reflという値を持つ。値を持つ型は恒真であると読み替えることができたから、すなわち、x = yという型が空でないことが、xとyが等しいことの証明になっている。

例えば、Idrisにおける、Listに対するhead函数は次のような型を持っている。

head : (l : List a) -> (isCons l = True) -> a

これは、第1引数にリストを取る他に、第2引数にそのリストがコンスセルである（Nilでない）「証明」を要求していることになる。もし isCons l = True が証明できなければ、そのような型を持つ値を渡すことができず、型が合わないから型検査時にエラーになる。

Idris> head [1, 2, 3] refl
1 : Integer
Idris> head [] refl
Can't unify x = x with isCons [] = True

Specifically:
	Can't unify False with True

so

もうひとつ、soというデータ型も紹介する。

data so : Bool -> Type where
  oh : so True

so Trueという型はohという値をもつ一方で、so Falseという型は空だ。実質的にso Pという型はP = Trueのことだと考えてよい。

参考文献