Agdaからはじまる関数脳で何かの夢を見る
先週はお世話になっている尼崎の産総研でAgda（アグダ）というプログラミング言語のチュートリアルがあり、火曜日から金曜日まで参加してきた。いちおうNAISTのプロジェクト実習という単位に充当されているのだが、参加者4人のうちNAIST生は私を入れて2人という非常にこじんまりとした会。先生陣が4人いて、ほぼマンツーマンで関数脳を鍛えられるという充実した時間だった。
Agdaはよく、「依存型（dependent type）付きの関数型プログラミング言語」と紹介されるようだが、今のぼくにはそれ以上のちゃんとした説明はできない。非常に表面的な説明をしておくと、Haskellでは表現できない∀とか∃といった論理記号に対応したプログラミング表現が可能な言語で、似たようなものにCoqがある。現状、何か実用的なソフトウェアで利用されているということはなく*1、まだ研究利用の段階にある未来言語だ。
まあ、それはともかくはじめてちゃんと関数型言語に触れたことで、頭が多少は関数脳になってきた。夏休みまで授業やら教科書講読やらで、論理学とか圏論とか集合論とかやってて一体これはどうつながるのか？というのが意味不明だったのだが、ああこれらはつながるのだが、ということがおぼろげながらつかめてきた。まだ完全に理解しているわけではないので鍛錬あるのみだが、どっかでブレイクスルーできそうな予感はする。
関数型言語といえば古くはLISP、現状Haskellが全盛で、その他ScalaとかOCaml、ML、Erlangなどなどようやく書店にも一般向けにいろいろ本が並び始めている面白い分野である。Agdaについての日本語での紹介はほとんどなく、今回のチュートリアルで使った印刷物がゆくゆくは出版予定ということだが、このブログでも折に触れて取り上げてゆきたい。
