プログラミング言語 idris

これは Theorem Prover Advent Calendar 2016 17日目の記事として書かれました.

idrisは依存型を持つ純粋関数型プログラミング言語です. ちなみにアイコンはこんな感じ.

f:id:wkwkes:20161215155232p:plain *1

今月の初め, バージョン 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 の証明はいくつか方法があります.

  • 示したいことを型にもつプログラムを直接書く.
    • 一番直接的な証明です. エディタのプラグインを使えば意外とシュッとかけます.
  • 対話的に証明する.
    • Coq のように対話的に証明を行えます. REPLから
      • :elab
      • :p

      のどちらかをタイプすることで対話環境に入ることができます. :elab は elaborator という idris に埋め込めるDSL的なもののスクリプトを生成します. :p も似たような証明のスクリプトを生成しますが現バージョンでは既に非推奨*2になっています.

証明のやり方がいくつかあって戸惑いますが, 少し触ってみたところ, 等式の証明をするときはプログラムを直接書くのがやりやすい. 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 -> AA の間の 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_p1Refl の型が推論してもらえず少し手こずりましたが, 他はすんなりいったと思います.

その他の話題

バックエンドがいろいろある

バックエンドというよりコンパイルのターゲットという方がいいかもしれません. Language Reference: Code Generation Targets にまとまっています. ここにも書き写しておきます.

Malfunction を経由して OCaml のバックエンドを利用する話は少し話題になっていた記憶があります.

エディタ

emacs, vim , atom あたりにはプラグインがあります. 型を書くとその実装の雛形を生成してくれたり, 簡単な証明を探索してくれたりして便利です. 詳しい説明は Theorem Proving: Pattern Matching Proofs にあります.

ちなみに私は emacs の idirs-mode を使いました.

おわりに

プログラミング言語の紹介と言いながら構文にほぼ言及しないなどよくわからない記事になりましたが, 参考になれば幸いです.

最後に参考にした・参考になりそうなページをあげて終わります.