依存型のあるプログラミング言語に慣れてみたいと思ってIdrisで遊んでみた。
依存型とは何かと言うと、普通の型付きラムダ計算はCurry-Howard対応によって直観主義命題論理に対応するが、依存型のあるラムダ計算は直観主義述語論理に対応する(という認識でいる)。
Curry-Howard対応によれば「型」は「命題」に対応する。そして、対応する論理は述語論理なので、「x=y」や「x≤3」のような、項を含む命題(型)を扱うことができる。Integer
型やString
型をもつ値はまあ分かるが、x=y や x≤3 という型をもつ値は一体何を表しているのかと思われるかもしれない。まあ「その命題が成り立つことの証拠、あるいは証明」だと考えればいいだろう。たぶん。
なんでIdrisをやろうかと思ったかというと、文法がHaskellに似ていて取っつきやすそうだったからである。ただ、まだまだ発展途上で実用するには向かなさそうだ。まとまったリファレンスマニュアルみたいなものは見つけられなかったので、標準ライブラリの細かいところはソースコードを参照した。また、この記事のコードはVersion 0.9.11.2に向けて書いてある。
今回はIdrisで自然数(Nat
型)を扱ってみる。最初の自然数0に対応するものは Z : Nat
である。ただし、型クラスがいい感じに定義されているので0
と書いても良い。自然数 x
の後続者(successor)は S x
である。さて、さっき命題の例として x≤3 と書いたが、Idrisには LTE : Nat -> Nat -> Type
というデータ構築子があって、自然数についての x≤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)∨(y≤x) に相当する。
LTE x y
型の値を作る(x≤y を証明する)には、2通りの関数(公理)がある。つまり、
lteZero : LTE Z y
、つまり 0≤ylteSucc : LTE x y -> LTE (S x) (S y)
、つまり x≤y→Sx≤Sy
だ。compareNats
の実装では x
と y
の値によって場合分けして、これらの関数を使って「証拠」を作ってやれば良い。
- y=0 の場合:
- (x<y)∨(y≤x) のうち y≤x が成り立つ。
LTE y x
型の値を返したいが、y=0 なのでlteZero
が欲しい型を持つ値である。 - したがって、
Either
のデータ構築子(∨ の導入則)と組み合わせて、Right lteZero
を返せば良い。
- (x<y)∨(y≤x) のうち y≤x が成り立つ。
- x=0,y=Sy′ の場合:
- (x<y)∨(y≤x) のうち x<y が成り立つ。したがって、
LT x y
型、つまりLTE (S Z) (S y')
型の値を返したい。 LTE Z y'
型の値であればlteZero
で得られた。これをlteSucc
に食わせてlteSucc lteZero
とすればLTE (S Z) (S y')
型の値が得られる。- したがって、
Either
のデータ構築子(∨ の導入則)と組み合わせて、Left (lteSucc lteZero)
を返せば良い。
- (x<y)∨(y≤x) のうち x<y が成り立つ。したがって、
- 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)∨(y≤x) のうち成り立つのは x<y の方なので、Left (lteSucc p)
を返せば良い。
compareNats x' y'
がRight q
を返してきた場合:q
は y′≤x′ の「証拠」である。これの両辺の後続者をとれば(両辺に1加えれば)、Sy′≤Sx′ の「証拠」、つまり y≤x の「証拠」になる。- つまり
lteSucc q
が y≤x の「証拠」である。(x<y)∨(y≤x) のうち成り立つのは y≤x の方なので、Right (lteSucc q)
を返せば良い。
- まず x′ と y′ を比較する。比較には
以上をまとめると次のようなコードになる:
[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(またはそれに類した言語)
- ペアノ算術
あたりの知識を仮定した。初心者向けではなく、自分のための備忘録的な感じで書いた。
ピンバック: Idrisの有界な自然数で遊んでみる(0) | 雑記帳