読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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

Agda Ubuntu

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

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

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

Agdaのインストール

AgdaEmacs上で動作する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すれば使えるようになる。