思いつきメモ Agda

まだExercise 1.5の続き。

tabulate : forall {n X} -> (Fin n -> X) -> Vec X n
tabulate {n} f = ?

を完成させる。{n}0としてC-cC-cをして、後はひたすらC-cC-aをすると、型としては正しい式が完成する。

tabulate {zero} f = <>
tabulate {suc y} f = f fzero , tabulate (\ _ -> f fzero)

というもの。fにずっとfzeroを与えたものをn個集めたVecを答えとしている。でも多分これは問題の答えとしては期待通りのものではない。イメージとしては、fにfzero, fsuc fzero, fsuc (fsuc fzero), ... を引数に与えたものをn個集めたものを得たい。つまり、f 0, f 1 ...

Dependently Typed Metaprogramming (in Agda) メモの続き。

Exercise 1.5では、有限集合を表す型Finを定義している。

data Fin : N -> Set where
   fzero : {n : N} -> Fin (suc n)
   fsuc : {n : N} -> Fin n -> Fin (suc n)

ここで、fzero, fsucとしたのは、自然数の型で使用しているzero, sucと区別しやすいようにするため。

有限集合Finは、依存型言語で良く取り上げられる例題のようだが、理解するのは簡単ではないように思う。次のように考えると良いと分かった：

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 ...