日々の流転

λ. WWW2005 1日目

朝ごはんは近くのロッテリアで食べた。

あうぅ。(経験者の)パートナーがいるはずだから何とかなるだろうと思ってたら、独りでアサインされてしまった。困った……、もう頭が真っ白ですよ。ぁぅぁぅ。至らないボランティア・スタッフでホント申し訳ないです。一日目にして早速逃げ出したくなってきた (T_T)

お昼は伊太利亜小料理 東風房というところでスパゲティを食べた。

夜はマハラジャというところで、インドカレー。美味しかった。

λ. Draft Agda Document, Agda-documentation team at AIST CVS

Draft Agda Document, Agda-documentation team at AIST CVS を読んで、例を色々試した。対話的な証明環境がとても面白い。以前にCoqを使ったときはゴールの管理が最初良くわからなくて困った記憶があるけど、Agdaのはとても分かりやすい。

Agdaではデータコンストラクタを使うときには、cons@_ のように、名前の後に @_ を付けなくてはならないけど、これは何故だろう?　ただし、パターンに書く場合には不要。何故こうなっているのだろう。むしろ、普通に使うときにはそのまま使えて、パターン内で使うときに(パターンによって束縛される変数と区別するために)特別な表記を用いるのが自然に思える。こうなっているのは型推論の都合?　caseの枝からcase対象の型を推論しないようになっていたり、型推論はHaskellとはちょっと違うところもあるので、その辺りが理由なのかな?

それから、現在のAgdalibはこのドキュメントとは多少異なっている部分もあった。たとえば、Existの定義は Exist (|X::Set)(P::Pred X) :: Set = Sum X P になっていて、型も (X::Set) |-> (P::X -> Set) -> Set になっている。(|->) の第一引数は暗黙のパラメタとなる型で、型推論によって与えられる?　普通に明示的に引数を渡そうとするとエラーになる。

それと、「compute to depth 100 by C-c *」と書いてあるけど、実際には C-c C-x + (agda-nfC100) なので注意。

λ. Ruby Magazine 0006号

.