プログラミング言語 idris
これは Theorem Prover Advent Calendar 2016 17日目の記事として書かれました.
idrisは依存型を持つ純粋関数型プログラミング言語です. ちなみにアイコンはこんな感じ.
今月の初め, バージョン 0.99 がリリースされました. 機能もほぼ安定したといことで これを機に少し遊んでみたのでその紹介をします.
はじめに断っておきますが, 私自身 idris を触って間もないのでおかしなことを書いている可能性があります. 間違い等あれば指摘していただければ幸いです.
処理系
brew install idris
などで降ってきます. idris
でREPLが起動します.
$ idris ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 0.99 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Idris is free software with ABSOLUTELY NO WARRANTY. For details type :warranty. Idris>
ghciに近い感覚で使えます. 複数行入力は :let
でできますが, やりにくいので一度ファイルにプログラムを記述してそれを読み込むのが無難だと思います.
実行ファイルが欲しければコマンドラインからidris -o hoge hoge.idr
などとすればOKです.
基本構文
だいたい Haskell です. 型クラス相当のものやdo
-notation まであります.
例えば 標準入力から受け取った文字列をそのまま出力するプログラムは次のように書けます.
main : IO () main = do x <- getLine putStrLn x
Haskellっぽいですね.
Haskell と違うところは Idris for Haskellers にまとまっていますが, すぐ気になるのは例えば
- 評価が正格
:
と::
が逆- 関数の型の記述が原則必須
などでしょうか.
また, 前述した通り idris には依存型があります.
たとえば伝統的な, 長さの情報をもつリストは次のように定義できます.
data Vect : Nat -> Type -> Type where Nil : Vect Z a (::) : a -> Vect k a -> Vect (S k) a
Vect
上の関数として例えば head
を書いておきます.
head : Vect (S n) a -> a head (x :: _) = x
依存型・証明
依存型といえば Coq や Agda が有名ですが, 定理証明支援系としての側面の強いそれらに対して, idris は依存型を用いた(通常の)ソフトウェア開発の可能性を探ることを目標にしているそうです.
とは言っても依存型がある以上, 証明的なものを書く必要が出てきます.
たとえば次の reverse
関数を考えます.
reverse : Vect n a -> Vect n a reverse x = reverse_ x Nil where reverse_ : Vect n a -> Vect m a -> Vect (n + m) a reverse_ Nil ys = ys reverse_ (x :: xs) ys = reverse_ xs (x :: ys)
よさそうに見えますが, コンパイルすると怒られます.
When checking right hand side of Main.reverse, reverse_ with expected type Vect (S k + m) a Type mismatch between Vect (k + S m) a (Type of Main.reverse, reverse_ a n x_shadow k (S m) xs (x :: ys)) and Vect (plus (S k) m) a (Expected type) Specifically: Type mismatch between plus k (S m) and S (plus k m)
コンパイラはplus k (S m)
と S (plus k m)
が等しくないと言っています. 愛くるしいですね.
ここでplus k (S m)
と S (plus k m)
が等しいことを証明する必要がありますが, idris の証明はいくつか方法があります.
- 示したいことを型にもつプログラムを直接書く.
- 一番直接的な証明です. エディタのプラグインを使えば意外とシュッとかけます.
- 対話的に証明する.
証明のやり方がいくつかあって戸惑いますが,
少し触ってみたところ, 等式の証明をするときはプログラムを直接書くのがやりやすい. elaborator は構文が大げさで使いにくい. :p
から入る証明モードが一番使いやすいと感じました.
遊んだ程度なので話半分に思ってください.
とりあえず plus k (S m)
と S (plus k m)
が等しいことを :elab
で証明してみます.
そのためにはまず証明する箇所をプログラム中に明示する必要があります.
reverse : Vect n a -> Vect n a reverse x ?= reverse_ x Nil where reverse_ : Vect n a -> Vect m a -> Vect (n + m) a reverse_ Nil ys = ys reverse_ (x :: xs) ys ?= reverse_ xs (x :: ys)
?=
に注意してください. これが証明する箇所を表します. 上のプログラムをREPLで実行すると
Idris> :l test.idr Holes: Main.reverse_lemma_1, Main.reverse__lemma_1
となって, ?=
に書き換えた証明すべきところが Holes
になっています.
idris では不完全な定義などが Holes
として明示されます.
REPLで :m
とすれば Holes
の一覧を見ることができます.
今から tactic を用いて Hole
を埋めていくことになります.
まず Main.reverse_lemma_1
を埋めましょう. :elab
コマンドで証明用のシェルに入ります.
*test> :elab Main.reverse_lemma_1 ---------- Goal: ---------- {hole0} : (a : Type) -> (n : Nat) -> Vect n a -> Vect (n + fromInteger 0) a -> Vect n a
Goal や 仮定 がでてきます.
tactic の詳細は :doc <tactic>
を見てください.
一気にやります. 雰囲気を感じてもらえれば.
-Main.reverse_lemma_1> intro' ---------- Assumptions: ---------- a : Type ---------- Goal: ---------- {hole0} : (n : Nat) -> Vect n a -> Vect (n + fromInteger 0) a -> Vect n a
-Main.reverse_lemma_1> intro' ---------- Assumptions: ---------- a : Type n : Nat ---------- Goal: ---------- {hole0} : Vect n a -> Vect (n + fromInteger 0) a -> Vect n a
-Main.reverse_lemma_1> intro' ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a ---------- Goal: ---------- {hole0} : Vect (n + fromInteger 0) a -> Vect n a
-Main.reverse_lemma_1> compute ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a ---------- Goal: ---------- {hole0} : Vect (plus n 0) a -> Vect n a
-Main.reverse_lemma_1> rewriteWith `(plusZeroRightNeutral ~(Var `{{n}})) ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a ---------- Goal: ---------- {hole0} : Vect (plus n 0) a -> Vect (plus n 0) a
-Main.reverse_lemma_1> attack ---------- Other goals: ---------- {hole0} ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a ---------- Goal: ---------- {hole1} : Vect (plus n 0) a -> Vect (plus n 0) a
-Main.reverse_lemma_1> intro' ---------- Other goals: ---------- {hole0} ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a value : Vect (plus n 0) a ---------- Goal: ---------- {hole1} : Vect (plus n 0) a
-Main.reverse_lemma_1> fill (Var `{{value}}) ---------- Other goals: ---------- {hole0} ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a value : Vect (plus n 0) a ---------- Goal: ---------- {hole1} : Vect (plus n 0) a =?= value
-Main.reverse_lemma_1> solve ---------- Assumptions: ---------- a : Type n : Nat x : Vect n a ---------- Goal: ---------- {hole0} : Vect (plus n 0) a -> Vect (plus n 0) a =?= \value => value
-Main.reverse_lemma_1> solve reverse_lemma_1: No more goals.
証明が終わったら:qed
コマンドで証明が出力されるのでそれをソースコードに貼り付ければ以降証明の必要はありません.
-Main.reverse_lemma_1> :qed Proof completed! Main.reverse_lemma_1 = %runElab (do intro' intro' intro' compute rewriteWith `(plusZeroRightNeutral ~(Var `{{n}})) attack intro' fill (Var `{{value}}) solve solve)
Main.reverse__lemma_1
も同じ要領でやった結果ソースコードは次のようになります.
reverse : {n: Nat} -> Vect n a -> Vect n a reverse x ?= reverse_ x Nil where reverse_ : {n: Nat} -> {m: Nat} -> Vect n a -> Vect m a -> Vect (n + m) a reverse_ Nil ys = ys reverse_ (x :: xs) ys ?= reverse_ xs (x :: ys) Main.reverse_lemma_1 = %runElab (do intro' intro' intro' compute rewriteWith `(plusZeroRightNeutral ~(Var `{{n}})) attack intro' fill (Var `{{value}}) solve solve) Main.reverse__lemma_1 = %runElab (do intro' intro' intro' intro' intro' intro' intro' intro' compute rewriteWith `(plusSuccRightSucc ~(Var `{{k}}) ~(Var `{{m}})) attack intro' fill (Var `{{value}}) solve solve)
型が通るのが確認できます.
Idris> :l test.idr *test>
以上が :elab
による証明の例でした.
対話的証明ではなく直接プログラムを書くスタイルのプログラム例も書いておきます.
とりあえず Reading HoTT in Coq の Coq のプログラムを参考に id : A -> A
が A
の間の equivalence になることを示してみました. (余分な関数も含まれています)
なお, 等式の証明についての詳しい説明は The Idris Tutorial: Thorem Proving などにあります.
total inverse : {A: Type} -> {x, y: A} -> (x = y) -> (y = x) inverse Refl = Refl total concat : {A: Type} -> {x, y: A} -> {z: A} -> (x = y) -> (y = z) -> (x = z) concat Refl Refl = Refl total concat_p1 : (A: Type) -> (x: A) -> (y: A) -> (p: x = y) -> (concat p Refl = Refl{x = x}) concat_p1 A x x Refl = Refl{x = (Refl{x = x})} total inv_inv : {A: Type} -> {x, y: A} -> (p: x = y) -> (inverse (inverse p)) = p inv_inv Refl = Refl total concat_assoc : (A: Type) -> (x: A) -> (y: A) -> (z: A) -> (w: A) -> (p: x = y) -> (q: y = z) -> (r: z = w) -> ((concat p (concat q r)) = (concat (concat p q) r)) concat_assoc A x x x x Refl Refl Refl = Refl total transport : {A: Type} -> {x, y: A} -> (P: A -> Type) -> (p: x = y) -> (u: P x) -> (P y) transport P Refl u = u total ap : {A, B: Type} -> {x, y: A} -> (f: A -> B) -> (p: x = y) -> (f x = f y) ap f Refl = Refl total apD : {A: Type} -> {B: A -> Type} -> {x, y: A} -> (f: (a: A) -> B a) -> (p: x = y) -> transport _ p (f x) = f y apD f Refl = Refl total sect : {A, B: Type} -> (A -> B) -> (B -> A) -> A -> Type sect s r x = r (s x) = x record IsEquiv (A: Type) (B: Type) (f: A -> B) where constructor BuildIsEquiv equiv_inv : B -> A eisretr : (x: B) -> sect equiv_inv f x eissect : (x: A) -> sect f equiv_inv x eisadj : (x: A) -> eisretr (f x) = ap f (eissect x) record Equiv (A: Type) (B: Type) where constructor BuildEquiv equiv_fun: A -> B equiv_isequiv: IsEquiv A B equiv_fun total idmap : (A: Type) -> A -> A idmap A = \ x : A => x isequiv_idmap : (A: Type) -> IsEquiv A A (idmap A) isequiv_idmap A = BuildIsEquiv (idmap A) (\ _ : A => Refl) (\ _ : A => Refl) (\ _ : A => Refl) equiv_idmap : (A: Type) -> Equiv A A equiv_idmap A = BuildEquiv (idmap A) (isequiv_idmap A)
concat_p1
の Refl
の型が推論してもらえず少し手こずりましたが, 他はすんなりいったと思います.
その他の話題
バックエンドがいろいろある
バックエンドというよりコンパイルのターゲットという方がいいかもしれません. Language Reference: Code Generation Targets にまとまっています. ここにも書き写しておきます.
Malfunction を経由して OCaml のバックエンドを利用する話は少し話題になっていた記憶があります.
エディタ
emacs, vim , atom あたりにはプラグインがあります. 型を書くとその実装の雛形を生成してくれたり, 簡単な証明を探索してくれたりして便利です. 詳しい説明は Theorem Proving: Pattern Matching Proofs にあります.
ちなみに私は emacs の idirs-mode を使いました.
無駄にカッコいい pic.twitter.com/NMHUsMo5E5
— わくわくエントリーシート (@wkwkes) 2016年12月13日
おわりに
プログラミング言語の紹介と言いながら構文にほぼ言及しないなどよくわからない記事になりましたが, 参考になれば幸いです.
最後に参考にした・参考になりそうなページをあげて終わります.
-
公式のチュートリアルです.
Edwin Brady: Archive for the ‘Idris’ Category
idrisの作者のページです.
REVERSE, REVERSE: THEOREM PROVING WITH IDRIS
idris での
reverse . reverse = id
の証明が書いてあります. エディタの使い方の例にもなっていて良いと思います.