依存型のあるプログラミング言語に慣れてみたいと思ってIdrisで遊んでみた。

依存型とは何かと言うと、普通の型付きラムダ計算はCurry-Howard対応によって直観主義命題論理に対応するが、依存型のあるラムダ計算は直観主義述語論理に対応する（という認識でいる）。

Curry-Howard対応によれば「型」は「命題」に対応する。そして、対応する論理は述語論理なので、「\(x=y\)」や「\(x\le 3\)」のような、項を含む命題（型）を扱うことができる。Integer型やString型をもつ値はまあ分かるが、\(x=y\) や \(x\le 3\) という型をもつ値は一体何を表しているのかと思われるかもしれない。まあ「その命題が成り立つことの証拠、あるいは証明」だと考えればいいだろう。たぶん。

なんでIdrisをやろうかと思ったかというと、文法がHaskellに似ていて取っつきやすそうだったからである。ただ、まだまだ発展途上で実用するには向かなさそうだ。まとまったリファレンスマニュアルみたいなものは見つけられなかったので、標準ライブラリの細かいところはソースコードを参照した。また、この記事のコードはVersion 0.9.11.2に向けて書いてある。

今回はIdrisで自然数(Nat 型)を扱ってみる。最初の自然数0に対応するものは Z : Nat である。ただし、型クラスがいい感じに定義されているので0と書いても良い。自然数 x の後続者(successor)は S x である。さて、さっき命題の例として \(x\le 3\) と書いたが、Idrisには LTE : Nat -> Nat -> Type というデータ構築子があって、自然数についての \(x\le 3\) という命題は LTE x 3 という型に対応する。LT : Nat -> Nat -> Type というものもあるが、これは LT x y = LTE (S x) y と定義されている。それぞれ、”Less Than or Equal to,” “Less Than” の略だと思われる。携帯電話の通信規格とは関係ない。

簡単な例として、二つの自然数を比較する関数を書いてみよう。普通の言語なら compareNats : Nat -> Nat -> Bool とでもするところだが、さっき書いたように「型は命題に対応」し、「値は証明、あるいは証拠を表す」と考えられるので、どうせなら「大きい方はどちらか、およびその証拠」を返す関数を作ってみよう。この関数の型は
[sourcecode lang=”plain”]
compareNats : (x : Nat) -> (y : Nat) -> Either (LT x y) (LTE y x)
[/sourcecode]
とする。この結果の Either (LT x y) (LTE y x) という型は、数学っぽく書けば \((x<y)\vee(y\le x)\) に相当する。

LTE x y型の値を作る（\(x\le y\) を証明する）には、2通りの関数（公理）がある。つまり、

• lteZero : LTE Z y、つまり \(0\le y\)
• lteSucc : LTE x y -> LTE (S x) (S y)、つまり \(x \le y \rightarrow Sx \le Sy\)

だ。compareNats の実装では x と y の値によって場合分けして、これらの関数を使って「証拠」を作ってやれば良い。

• \(y=0\) の場合:
  • \((x<y)\vee(y\le x)\) のうち \(y \le x\) が成り立つ。LTE y x 型の値を返したいが、\(y=0\) なので lteZero が欲しい型を持つ値である。
  • したがって、Eitherのデータ構築子（\(\vee\) の導入則）と組み合わせて、Right lteZeroを返せば良い。
• \(x=0, y=S y’\) の場合:
  • \((x<y)\vee(y\le x)\) のうち \(x<y\) が成り立つ。したがって、LT x y 型、つまり LTE (S Z) (S y') 型の値を返したい。
  • LTE Z y' 型の値であれば lteZero で得られた。これを lteSucc に食わせて lteSucc lteZero とすれば LTE (S Z) (S y') 型の値が得られる。
  • したがって、Eitherのデータ構築子（\(\vee\) の導入則）と組み合わせて、Left (lteSucc lteZero)を返せば良い。
• \(x=Sx’,y=Sy’\) の場合:
  • まず \(x’\) と \(y’\) を比較する。比較には compareNats x' y' が使える。
  • compareNats x' y' が Left p を返してきた場合:
    • p は \(x’ < y’\) の「証拠」である。これの両辺の後続者をとれば（両辺に1加えれば）、\(Sx'<Sy’\) の「証拠」、つまり \(x<y\) の「証拠」になる。
    • つまり lteSucc p が \(x<y\) の「証拠」である。\((x<y)\vee(y\le x)\) のうち成り立つのは \(x<y\) の方なので、Left (lteSucc p) を返せば良い。
  • compareNats x' y' が Right q を返してきた場合:
    • q は \(y’ \le x’\) の「証拠」である。これの両辺の後続者をとれば（両辺に1加えれば）、\(Sy’\le Sx’\) の「証拠」、つまり \(y\le x\) の「証拠」になる。
    • つまり lteSucc q が \(y\le x\) の「証拠」である。\((x<y)\vee(y\le x)\) のうち成り立つのは \(y\le x\) の方なので、Right (lteSucc q) を返せば良い。

以上をまとめると次のようなコードになる:
[sourcecode lang=”plain”]
compareNats : (x : Nat) -> (y : Nat) -> Either (LT x y) (LTE y x)
compareNats x Z = Right lteZero
compareNats Z (S y’) = Left (lteSucc lteZero)
compareNats (S x’) (S y’) = case compareNats x’ y’ of
Left p => Left (lteSucc p)
Right q => Right (lteSucc q)
[/sourcecode]
あるいは、either : (a -> c) -> (b -> c) -> (Either a b) -> c 関数を使えば次のようにも書ける:
[sourcecode lang=”plain”]
compareNats : (x : Nat) -> (y : Nat) -> Either (LT x y) (LTE y x)
compareNats x Z = Right lteZero
compareNats Z (S y’) = Left (lteSucc lteZero)
compareNats (S x’) (S y’) = either (Left . lteSucc) (Right . lteSucc) (compareNats x’ y’)
[/sourcecode]

今回はここまで。

なお、今回の記事では

• Curry-Howard対応
• Haskell（またはそれに類した言語）
• ペアノ算術

あたりの知識を仮定した。初心者向けではなく、自分のための備忘録的な感じで書いた。