日々の流転

λ. Agda2

ずっとAgda2を試そう試そうと思っていたけど、ようやく試した。

まずはインストール。alexとhappyはwindows用のバイナリをダウンロードしてきてPATHの通っている場所に置く。binaryとzlibはまだGHC 6.8対応していないようだったから自分で対応して……とかやってるうちに対応版が出ていた。しょぼーん。Agda2自体も簡単なパッチ(Agda-2.1.2-ghc68-win32.patch)をあててビルドできた。

で、動かしてみる。 Agda1はemacs-agdaというプログラムとelispが通信していたけど、Agda2ではhaskell-modeで動かしたghciにライブラリを読み込ませて、こいつとやり取りをして実現している。これは面白い。よく考えたなぁ。ただ、実行環境を配布したりするのにはちょっと面倒になってしまっているけど。

とりあえず、かなり色々変わっているようなので、色々試してみる。

文法

まずは文法。型宣言に使う記号が「::」から「:」になっていて*1、暗黙の引数は「{A : Set} ->」等として渡すようになっている。 恒等関数はこんな感じになる。

id : {A : Set} -> A -> A
id x = x

嵌ったのがcase。以下の状態でゴール0で C-c C-c で agda2-make-case を呼び出すと「Panic: passAVar: got x」というエラーになる。 サンプルを見てもcaseを使ったのはないみたいだし、caseはなくなったのだろうか。

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

f : Nat -> Nat
f x = { x }0

また、この例のようにデータ型定義はGADTスタイルになり、dataとidataの区別も無くなったようだ。 (2007-12-08追記: というか、The Agda Wiki - Inductive Families を見ると、Inductive Families は無くなっているのね。これはAgda1からの乗り換えはまだ難しいか)

それから、演算子の定義でアンダースコアをプレースホルダーとして使うことが出来るようになっていて、中置演算子だけでなく、distfix な演算子も簡単に定義可能。OBJみたいでかっこいい。けど、アンダースコアを含む名前が使えなくなっているので注意。

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

しかし、こうしてみてみると、Haskellに囚われずに文法を拡張していってるんだなぁ、と思う。

停止性検査

それから、停止性検査のagda-check-terminationコマンドはなくなっているので、その辺りはどうなっているのかと思い、以下の例を試す。 そしたら、一行目のbottomと二行目の右辺のbottomが赤くハイライトされた。なるほど、自動的に検査されるようになったのね。

bottom : {A : Set} -> A
bottom = bottom

次はアッカーマン関数を試す。今度は赤くハイライトされない。 Agda1よりは強力なアルゴリズムを使っているようだ。 Size Change Termination (SCT)?　 (2008-03-24 追記: アッカーマン関数のAgdaでの定義 - あいまいな本日の私(2008-03-11)によると、アルゴリズム自体はfoetusの停止判定で変わらず、単にAgda1で実装がまだ追いついていなかったということらしい)

ack : Nat -> Nat -> Nat
ack (zero) n            = suc n
ack (suc m') (zero  )   = ack m' (suc zero) 
ack m@(suc m') (suc n') = ack m' (ack m n')

次に、20050508にAgda1を触ったときにも試した、再帰的なデータ型を試す。結果は「Datatype T is not strictly positive, because it occurs negatively」というエラーになった。正しい対処だとは思うが、HOASを使いたい人とかには残念かもね。

data T (P : Set) : Set where
  psiInv : (T P -> P) -> T P

型クラス

Agda1にあった型クラスは無くなった? examples/Monad.agda にモナドを定義する例があるが、これに関しては以前に比べると非直観的なような。

Prop≠Set

以前に池上さんに教えてもらったように、Setとは別にPropというソートが用意されていて、型の階層は以下のようになっている。 ただ、PropとSetをどう使い分ければ良いかはまだ良くわからない。

• Prop ⊂ Set1
• Set ⊂ Set1
• Set1 ⊂ Set2 ⊂ …

相互再帰

Agda1では定義の中では既に定義済みの定義と自分自身しか参照できなかったため、相互再帰を行いたいときは自分で組化(tupling)を行う必要があった。 それに対して、Agda2ではmutualキーワードを使って相互再帰的な定義を自然に行えるようになっている。

mutual

  even : Nat -> Bool
  even zero    = true
  even (suc n) = odd n

  odd : Nat -> Bool
  odd zero    = false
  odd (suc n) = even n

【2007-12-08追記】 これは勘違い。私が知らなかっただけで、Agda1のころからmutualはあった。