agdaに挑戦し、即死した話
agdaは公式のチュートリアル(http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)に日本語の記事があったので、それをやることにした
http://ocvs.cfv.jp/tr-data/PS2008-014.pdf
こいつだ。
その前にまずagdaのインストールをする。
agdaはcabalでinstallできる。
haskellの環境は整っていたので、さくっとcabal install agdaで入ると思ったが、なんか引っかかって入らない。
haskellの環境は今特に使っておらず消えてもいいのでcabal関連全消しして、
http://ghcformacosx.github.io/
こいつを入れることにした。
もうなんかめんどくさいからこれでいいや的な。
便利。
これを入れてパスを通して、時間はかかるもののagdaのinstallは完了。
次のハードルはemacs !!
僕は完全なるvimユーザで、間違ってEDITORがemacsの状態で何かを開いてしまうとググらないと何もせず穏便に終了することもできないくらいにはemacsがわからない。
vimでやれないかと探してみると、ないことはないが若干心配なレベル
https://github.com/derekelkins/agda-vim
開発はactiveなようなので見守りはしていこうと思った。
仕方なくemacsを覚えることに。
これはまた別の記事にする.
ページにしてわずか6ページ目のこの部分にして
data ⊥ : Set where ⊥ Elim : {P : Prop} -> ⊥ -> P ⊥ Elim ()
More than one matching type signature for left hand side ⊥ Elim () it could belong to any of: Elim ⊥
という渡しには解読不能なエラーに遭遇する
ぐぐってもわからない。
説明を読む限りではどんな型にもマッチし得ない関数を書いたつもりなのだが、1つ以上の型シグニチャにマッチするんだとは・・?とか英語力もなくtype signatureとかの理解も浅く早速行き詰まってしまう。
さっぱりわからんわーと思っていたところで↓この記事に出会う。
http://d.hatena.ne.jp/Lost_dog/20131202/1385995897
(もう少し証明関連で日本語記事を漁れ、という感じだったか・・・)
そしてこの2文にぴーんとくるわけです
そもそも文法もわかっていないけど、定理証明が何だかが全くわからないと思っていた。なるほどCoqのテキストを読むんだな!と
ここまでくると、なんとなくAgdaの文法が分かってきた頃と思います。しかし文法だけ分かっても、定理証明とは何なのかが分からないと、何がなんだかさっぱりのはずです。そして、そういった内容のAgdaのテキストは、今のところありません! じゃあどうするかというと、Coqのテキストを読むのです。Coqのテキストはそれなりに充実していて、色々あるようですが、日本語で、ネットで読めるという、素晴らしいものが『ソフトウェアの基礎』です。notogawaさんがAgda版コードを公開しています。ちなみに、これをテキストにしたCoq勉強会がまさに今開かれています。
ということでAgdaは諦めてCoqをやることにする。
少し知識を深めてAgdaに戻ってこようと思うが、ひとまずCoqをやろう。
そんな証明初日。