Agda(Agda2.2.4)をインストールして hello worldプログラムを書いてみた。OSのディストリビューションは最近リリースされた Ubuntu 9.10。 非常に簡単にインストールができたので、依存型erのみんなは Ubuntu 使うといいよ。 Agdaのインストール Agdaの標準…

最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるの…