ほんとうはこわいIdris 〜 tacticメタプログラミング

はじめに

Idris分からん! 誰か教えてくれー

こわくないIdris

Idrisについて全く知らないって人は、僕が以前書いた記事を読んでください。
こわくない Idris で M59のブログ を検索

tacticとは

カリー゠ハワード同型対応があるからプログラムを書くことがそのまま証明を書くことになるのだが、それとは別に定理証明器のとるべき戦略=tacticを記述することによっても証明を書くことができる。

Coqのtacticと比べるとIdrisのそれはとても貧弱に見える。前試したときは、自分でプログラム書いて証明した方がまだ楽なんじゃないかと思った。

tacticメタプログラミング

Language.Reflectionモジュールを使うと、tacticを生成する関数を定義できる。例えば、Data.Vectモジュールに定義されているfindElemがある。

Elem

その前に、Elemというデータ型について書いておこう。

using (xs : Vect k a)
  data Elem : a -> Vect k a -> Type where
    Here : Elem x (x::xs)
    There : Elem x xs -> Elem x (y::xs)

Elem t ts というのは t ∈ ts という命題を表すデータ型だ。定義は、Elem t tsが成り立つのは Here : Elem x (x::xs) と There : Elem x xs -> Elem x (y::xs)という2通りのケースがあると読める。具体例を示そう。

*Vect> the (Elem 'a' ['a', 'b', 'c']) Here
Here : Elem 'a' ['a','b','c']
*Vect> the (Elem 'b' ['a', 'b', 'c']) (There Here)
There (Here) : Elem 'b' ['a','b','c']
*Vect> the (Elem 'c' ['a', 'b', 'c']) (There (There Here))
There (There (Here)) : Elem 'c' ['a','b','c']

型Elem 'a' ['a', 'b', 'c']が表す命題は真で、それを証明するのはデータHereだ。同様に、命題Elem 'b' ['a', 'b', 'c']には証明There Hereが、Elem 'c' ['a', 'b', 'c']には証明There (There Here)が与えられる。このように、命題が真のときは、真である証明となるデータが構築できる。型検査によって、これらが正しい証明になっていることが保証される。

findElem

関数findElemが生成するtacticは、Elem t tsの証明となるデータを見つけ出す。

findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
findElem Z ctxt goal = Refine "Here" `Seq` Solve
findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

試行の上限回数を与えると、その回数まで Here, There Here, There (There Here) ... という証明を試しているようだ。型推論時には停止しないプログラムが使えないので、試行の上限回数を指定し、有限回の試行で停止させる必要がある。

HVect

このfindElemは、Data.HVectモジュールで使われている。

using (k : Nat, ts : Vect k Type)
  data HVect : Vect k Type -> Type where
    Nil : HVect []
    (::) : t -> HVect ts -> HVect (t::ts)

  get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
  get {p = Here} (x::xs) = x
  get {p = There p'} (x::xs) = get {p = p'} xs

  put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
  put {p = Here} y (x::xs) = y :: xs
  put {p = There p'} y (x::xs) = x :: put {p = p'} y xs

  update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
  update {p = Here} f (x::xs) = f x :: xs
  update {p = There p'} f (x::xs) = x :: update {p = p'} f xs

HVectは型の異なるデータを持つことができるベクターだ。HVectを操作するget/put/update関数が用意されている。これらの関数は、{default tactics { applyTactic findElem 100; solve; } p : Elem t ts}という暗黙の引数を取っている。defaultが指定されていると、指定されたtacticsによって、この引数を自動的に補うようになる。つまり、自動的にElem t tsを証明するわけだ。証明はベクターのインデックスそのものだから、インデックスを指定することなく型の適合するデータに対して操作できることになる。

*HVect> the Nat (get ['a', "hello", Z])
0 : Nat
*HVect> the String (get ['a', "hello", Z])
"hello" : String
*HVect> the Char (get ['a', "hello", Z])
'a' : Char
*HVect> the String (get ['a', "hello", Z])
"hello" : String
*HVect> the Nat (get ['a', "hello", Z])
0 : Nat
*HVect> put 'b' ['a', "hello", Z]
Data.HVect.:: 'b' (Data.HVect.:: "hello" (Data.HVect.:: 0 Data.HVect.Nil)) : HVect [Char,String,Nat]
*HVect> put "world" ['a', "hello", Z]
Data.HVect.:: 'a' (Data.HVect.:: "world" (Data.HVect.:: 0 Data.HVect.Nil)) : HVect [Char,String,Nat]
*HVect> put (S Z) ['a', "hello", Z]
Data.HVect.:: 'a' (Data.HVect.:: "hello" (Data.HVect.:: 1 Data.HVect.Nil)) : HVect [Char,String,Nat]
*HVect> update S ['a', "hello", Z]
Data.HVect.:: 'a' (Data.HVect.:: "hello" (Data.HVect.:: 1 Data.HVect.Nil)) : HVect [Char,String,Nat]
*HVect> update (++ "world") ['a', "hello", Z]
Data.HVect.:: 'a' (Data.HVect.:: "helloworld" (Data.HVect.:: 0 Data.HVect.Nil)) : HVect [Char,String,Nat]

こわいですね。

Effects

EffectsモジュールでもLanguage.Reflectionを使っているみたいです。

まとめ

型推論器の力を使って、証明を自動で行わせることで、すごいことができる。これは型推論時実行といえる。深い闇を感じる。