Dependently Typed Metaprogramming (in Agda) メモ
Dependently Typed Metaprogramming (in Agda)のメモ
Agdaの編集方法：
Emacsのagda-modeを使えば、TeXの感覚で記号を入力できる。例：
太字のN : \bn
下付の数字 : _0, _1など
× : \times
→ : \rightarrow
それと型構成子×は、open import Data.Productを書かないと使えなかった。また、最初はData.Productが開けなかったので、(custom-set-variables '(agda2-include-dirs (quote ("." "agda-lib-folder/src"))))を.emacs.elに追加する必要があった。
------------------------------------
C-cC-lで現在開いているagdaファイルをロードしてチェックしてくれる。
zip : forall {n S T} -> Vec S n -> Vec T n -> Vec (S × T) n
zip ss ts = ?
上のように、関数の型定義のみを記述し、関数の本体定義の右側に?を入れてからロードすると、対話的に証明が出来る。
zip ss ts = { }0
となり、 ?0 : Vec (.S × .T) .nと情報が表示される。これは{}0の場所に、型Vec (.S × .T) .nを持つ式を記述すればよい、ということを示している。
{}0の中にssを入力し、C-cC-cをすると、ssについて場合分けができる。{}の中が自明であれば、この中でC-cC-aをすると、型に合う式を見つけて、自動的に式を作ってくれる。
既に定義した名前を{}に入れてからC-cC-aすると、それらの名前もヒントとして使用してくれる(Exercise 1.3. vapp vecと書いてからC-cC-aで埋めてくれる。Exercise 1.4もvapp vecを書くだけでvapp (vapp (vec ,) ss) tsと埋めてくれる)
とりあえず、今回はここまで。