Idris でカリー・ハワード対応をより実践的に理解しようっていう記事です。
ざっくり言うと、命題を型に対応させることで証明とプログラミングが対応するということです。逆に言えば**プログラミングとは証明だったのだ…！**という数学科出身の僕にとっては歓喜の事実です。
型が first class
Idris では型が first class です。型を値と同列に扱うことが出来るので、型を返す関数や型を引数に取る関数も定義出来ます
a : Type
a = String
foo : Bool -> Type
foo True = Int
foo False = String
nFoldList : Nat -> Type -> Type
nFoldList Z t = t
nFoldList (S n) t = List (nFoldList n t)
Nat というのは自然数の型で、 Z : Nat と S : Nat -> Nat というコンストラクタを持ちます。
Z は 0 を表す値で、 S は successor を表す関数です。つまり S n は n + 1 のこと。
上の nFoldList は n重リストの型の定義になります。再帰関数で型を定義出来るわけです。
命題と型が対応する
これは実例を見るとわかりやすいと思います。
OneIsOne : Type
OneIsOne = 1 = 1
OneIsTwo : Type
OneIsTwo = 1 = 2
OneIsOneOrTwo : Type
OneIsOneOrTwo = Either OneIsOne OneIsTwo
OneIsOneAndTwo : Type
OneIsOneAndTwo = Pair OneIsOne OneIsTwo
1 = 1 や 1 = 2 は型です。関数定義の = と並んでいて微妙に分かりづらいかもしれませんが…
OneIsOne は 1 = 1 という型で、そのまま「1 = 1」という命題に対応します。
OneIsTwo も同様に「1 = 2」という命題に対応します。
OneIsOneOrTwo は「1 = 1 または 1 = 2」という命題に対応します。
OneIsOneAndTwo は「1 = 1 かつ 1 = 2」という命題に対応します。
次の節でもう少し詳しく話します。
命題が真 ⇔ 型が値を持つ
x = x という等式型には唯一 Refl という値があります(反射律 = Reflexivity)。
一方で、 x ≠ y のときには x = y という型に値は存在しません。
このように、命題が真であることと、型に値が存在することが対応します。
逆に言えば、値はその型が真であることの証明であると言えます。
上の例で言えば OneIsOne すなわち 1 = 1 という型には Refl という値が存在し、
OneIsTwo すなわち 1 = 2 という型には値が存在しません。
OneIsOneOrTwo すなわち Either (1 = 1) (1 = 2) には Left Refl という値が存在します。
従って Either は論理和に対応することがわかります。
OneIsOneAndTwo すなわち Pair (1 = 1) (1 = 2) には第二要素になれる値が存在しないため、値が存在しません。
従って Pair は論理積に対応することがわかります。
関数型と関数適用
上記の考え方をすると、関数型 A -> B は 「A ならば B」という命題に対応します。
A -> B の型を持つ関数 f があり、かつ A に値 a があれば、f a という B の型を持つ値があることになるからです。
これはちょうど関数適用が modus ponens
((A ⇒ B) ∧ A) ⇒ B
に対応することを意味しています。
プログラミングは証明である
つまり「A ならば B である」という命題を証明することは、型 A -> B を持つ関数を作ることに対応するわけです。
プログラミングというのは関数を作ることなので、プログラミングとは証明であるということが分かってしまいました。
ここで特筆すべきことは、作った値がその型を持つことはコンパイラがチェックしてくれるということです。すなわちコンパイラが証明の正しさを保証してくれるのです！
依存型
とはいえ量化記号(∀と∃)が使えなければ証明など出来るはずもありません。これらに対応するのが依存型なわけです。
$^\forall a \in A, P(a)$ という命題は Idris の型として書くと (a: A) -> P a
$^\exists a \in A, P(a)$ という命題は Idris の型として書くと (a: A ** P a)
となります。
否定
もちろん否定が出来なければ証明など出来ません。
Idris には Void という値の無い型が存在します。これは$\bot$に対応するものですが、命題に対する否定は
Not : Type -> Type
Not a = a -> Void
と定義されています。直訳すれば「a が真であるなら矛盾する」ということですね。
証明してみる
例としてド・モルガンの法則(の一部)「$¬(a ∨ b) \implies (¬a) ∧ (¬b)$」を証明してみましょう。
まずは命題を型に直します。
¬a は a -> Void
a ∨ b は Either a b
a ∧ b は Pair a b
であったことに注意すると
deMorgan : ((Either a b) -> Void) -> Pair (a -> Void) (b -> Void)
となりますね。次にこの関数を実装していきましょう。
この関数は (Either a b) -> Void の型の関数を受け取って Pair (a -> Void) (b -> Void) を返す関数です。
とりあえず引数を取ってみましょう:
deMorgan : ((Either a b) -> Void) -> Pair (a -> Void) (b -> Void)
deMorgan f = ?dm
a -> Void と b -> Void の値を両方作りたいので、a の値から Void を作る関数、b の値から Void を作る関数が欲しいところです。
ここで f は Either a b -> Void という型なので、 a -> Either a b や b -> Either a b という型の関数があれば f と合成して a -> Void, b -> Void が作れそうです。
Left : a -> Either a b, Right : b -> Either a b がまさにそれですね。ということで
f . Left が a -> Void, f . Right が b -> Void の型を持つことになります。
deMorgan : ((Either a b) -> Void) -> Pair (a -> Void) (b -> Void)
deMorgan f = ((f . Left), (f . Right))
これでコンパイルが通りました。証明終了です。
興味を持った方はぜひこの命題の逆「$(¬a) ∧ (¬b) \implies ¬(a ∨ b)$」を証明してみてください。