Idris で理解するカリー・ハワード対応

Idris で[カリー・ハワード対応](https://www.wikiwand.com/ja/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C)をより実践的に理解しようっていう記事です。

ざっくり言うと、命題を型に対応させることで証明とプログラミングが対応するということです。逆に言えば**プログラミングとは証明だったのだ…！**という数学科出身の僕にとっては歓喜の事実です。

# 型が first class

Idris では型が first class です。型を値と同列に扱うことが出来るので、型を返す関数や型を引数に取る関数も定義出来ます

```idris
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重リストの型の定義になります。再帰関数で型を定義出来るわけです。

# 命題と型が対応する

これは実例を見るとわかりやすいと思います。

```idris
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](https://www.wikiwand.com/en/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$に対応するものですが、命題に対する否定は

```idris
Not : Type -> Type
Not a = a -> Void
```

と[定義されています](https://github.com/idris-lang/Idris-dev/blob/0417c53fb6b91fc0692245f269b98a3bd4820136/libs/prelude/Prelude/Basics.idr#L7)。直訳すれば「a が真であるなら矛盾する」ということですね。

# 証明してみる

例としてド・モルガンの法則(の一部)「$¬(a ∨ b) \implies (¬a) ∧ (¬b)$」を証明してみましょう。

まずは命題を型に直します。
¬a は `a -> Void`
a ∨ b は `Either a b`
a ∧ b は `Pair a b`
であったことに注意すると

```idris
deMorgan : ((Either a b) -> Void) -> Pair (a -> Void) (b -> Void)
```

となりますね。次にこの関数を実装していきましょう。
この関数は `(Either a b) -> Void` の型の関数を受け取って `Pair (a -> Void) (b -> Void)` を返す関数です。
とりあえず引数を取ってみましょう:

```idris
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` の型を持つことになります。

```idris
deMorgan : ((Either a b) -> Void) -> Pair (a -> Void) (b -> Void)
deMorgan f = ((f . Left), (f . Right))
```

これでコンパイルが通りました。証明終了です。

興味を持った方はぜひこの命題の逆「$(¬a) ∧ (¬b) \implies ¬(a ∨ b)$」を証明してみてください。