日々の流転

λ. PM 4時まで寝てた。

λ. 海の上のピアニスト

ケーブルテレビで「海の上のピアニスト」を見た。とても素敵な映画だった。

λ. Delphi

Delphi 6 Personalを入れた。久しぶりのDelphi。どうせだから後でApolloも試してみよと。

λ. ウィルス

SFCでもウィルス流行ってるみたい。Outlook Express ユーザが被害にあうのは、自業自得みたいなもんだから知ったこっちゃないけど、ごみメールをばら撒くのはウザイよなー。せめて、相手がOutlook Expressを使ってるか確認してから送るとか出来んのだろうか。

λ. WString 0.0.3

ふむふむ。こないだのパッチ([ruby-ext:2005]のwstring-wctrans.diff)はstd::unary_function<wchar_t, wchar_t>を継承すれば良かったのか。なるほど。勉強になるなぁ。

λ. 師走です。でも私は走りません。当然です。

λ. お昼

みのり亭

λ. 計画停電

学校が計画停電でした。停電の事自体は覚えていたのだけど、学校のサーバが使えなくなるのは思いの外不便だった。

λ. 借りた本

『仙姫午睡(せんきごすい)』

桂木祥[著] 珠黎皐夕(しゅれいこうゆ)[イラスト]

『細菌人間』

筒井康隆[著]

『ぼくらは虚空に夜を視る』

上遠野浩平[著] 中澤一登[イラスト]

小説すばる 2002年7月号

-

λ. ソ◯ロ◯

をネタにするというのは一体誰が始めたのだろう。と、ふと思った。

λ. 『壷中の天国』 倉知 淳

を読了。

λ. 随伴とモナド

半順序集合(N,≦)の上の随伴でちと面白いと思った例。

• p(n)≦m ⇔ n≦g(m)
• p(0) = 0
• p(n) = n番目の素数
• g(m) = m以下の素数の数

擬順序(preorder)上のモナドは closure operator と呼ばれる。

• a≦T(a)
• T(T(a)) ≦ T(a)

半順序集合の場合には T(T(a))=T(a) が言える。

λ. 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はあった。