Getting Started with Agda アグダを始めよう

Agda Ubuntu

Agda(Agda2.2.4)をインストールして hello worldプログラムを書いてみた。

OSのディストリビューションは最近リリースされた Ubuntu 9.10。
非常に簡単にインストールができたので、依存型erのみんなは Ubuntu 使うといいよ。

  • Agdaのインストール
  • Agdaの標準ライブラリを使えるようにする
  • Agdaでhello, world

Agdaのインストール

AgdaはEmacs上で動作するagda-modeをインストールすれば使えるようになるみたいだ。
agda-modeはapt-getで簡単にインストールできた。

$ sudo apt-get install agda-mode
以下のパッケージが新たにインストールされます:
  agda-mode cpp-4.1 emacs emacs22-bin-common emacs22-common emacs22-gtk
  emacsen-common g++-4.1 gcc-4.1 gcc-4.1-base ghc6 haskell-mode libffi-dev
  libghc6-agda-dev libghc6-binary-dev libghc6-haskeline-dev
  libghc6-haskell-src-dev libghc6-mtl-dev libghc6-quickcheck2-dev
  libghc6-terminfo-dev libghc6-utf8-string-dev libghc6-xhtml-dev
  libghc6-zlib-dev libgmp3-dev libgmpxx4ldbl libncurses5-dev
  libstdc++6-4.1-dev zlib1g-dev

ghcやemacsどころか、まだgccすらなかったのでたくさんインストールをがんばってもらった。

Agdaの標準ライブラリを使えるようにする

現時点でのAgda(Agda2.2.4)では標準ライブラリが一緒ではないみたいだったので、Agda本家からダウンロードした。
入手したライブラリを実際に使うためにはパスを通す必要がある。README.agdaに「(M-x customize-group RET agda2 RET)というEmacsコマンドを実行してね」と書いてあったのでそうしてみた。そこで、"Agda2 Include Dirs"という項目にライブラリのsrcというパスを絶対パスで指定すれば使えるようになった。
使い方はAgdaのコードで

import Data.Nat as N
open import Data.List
open import Data.String

とかいう風に書けばいいみたいだ。

Agdaでhello, world

じゃあ、早速Agdaでプログラムしてみよう！なんてったってAgdaはプログラミング言語だもんね。
文字列を標準出力に出力するプログラムhello.agdaは以下のように書ける。

module hello where

open import IO

main = run (putStrLn "Hello, あぐだworld!")

(C-c C-l)というコマンドを打てば、ソースコードに誤りがないか型チェックしてくれる。さらに、(C-c C-x C-c)コマンドでコンパイルすることもできる。
hello.agdaをコンパイルするとhelloという名前の実行ファイルができた。実行してみよう。

  $ ./hello
Hello, あぐだworld!

日本語もばっちりだ。こんにちはアグダ。こんにちは依存型。

ちなみにemacsを使わないコンパイラもあって、Ubuntuではagda-binというパッケージをapt-getすれば使えるようになる。