日々の流転

λ. Javaではclosureの代わりに無名クラスというのがあるらしい。

λ. SFC-MODE/NNTP

上の「最近のツッコミ」は都合によりその月の分しか表示していないのだけど、例の構想についてtakotさんという方にツッコミもらった。

とりあえず、データを取ってくるコードはそれなりで、今はNNTPについて勉強中。

λ. 人間と法

法哲学の話ですらないような「話を聞かない男、地図が読めない女」の話なんてどうでも良い。もっと役に立つことを話してくれ。

λ. 今日の向井研

チャネル理論のタイプレベルのインファレンスがグローバルカットに関係しているらしい。

それから、こないだ考えたclassificationの圏のcoproductは、most general refinement なチャネルのcoreという意味があるらしい。

あと、僕はこれまでこの日記では f_typとf_tokと書いていたけど、本当はf^∧とf^∨と書くらしい。

λ. TOEFL

学校でTOEFLの試験を受けてくる。だるい。

λ. 『素敵なお店のかわいい制服』

を読んだ。

λ. 1bitの情報量

* 今日の一言:
「1bitの情報量は，ちょびっと」 by 服部先生
直後，時間が止まった．

一瞬、ちょびっツ と誤読。

λ. 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号

.

λ. ロバ文と依存型と

「Every farmer who owns a donkey beats it.」のような文をロバ文(donkey sentence)といい、一階述語論理の限量子では適切に量化出来ない例として良く知られている。が、ふとこれは依存型の存在するある種の型理論で「∏x:(∑f:Farmer. ∑d:Donkey. own(f,d)). beat(p1(x), p1(p2(x)))」みたいに表現すればいいじゃんと気づいた。

でも、喜んだのは一瞬だけで、調べたらそんなアイディアは Ranta さんらによってとうにやりつくされているのでした。俺なんかがふと思いつく程度のアイディアは誰かにやられていて当たり前だけどね。たはは。

しかし、強力な型理論で自然言語の意味論を扱うのは結構面白そうだ。それに、考えてみればMontagueの理論は個体,真理値,内包的指標からなる単純型付きラムダ計算に基づいていると言えるわけで、この方向は必然だったとも思う。

λ. 鳳梨酥

台湾のお土産らしい。

λ. 大分四日目

実習生の同じ班の人たちで、湯布院まで遊びに行ってきた。

お昼を茄子屋というところで食べ、夢想園というところで温泉に漬かってきた。

平日だったということもあるのだろうが、あまり観光地っぽいギラギラした感じもなく、落ち着いた良いところだった。

λ. Chapter 9 の練習問題4

準開基(subbasis)の各有限部分集合のmeetは開基(basis)になる。なので、可算な準開基があるならば開基も可算*1になる、つまり位相空間は second countable になる。……この練習問題簡単すぎじゃない?

λ. Scala勉強会＠関東-1

水島さん企画のScala勉強会に参加。 企画の存在は覚えていたのだけど、参加表明が必要なことを見落としていることに前日気づく。結局、キャンセルがあったため参加することが出来た。

水島さんの発表「Scalaチュートリアル」が発表40分なのに、皆がツッコミを入れまくって2時間以上になっていてウケた。水島さん独演ショー。 水島さんの発表ではScalaがいかに節操のない言語*1かを理解することが出来、soutaroさんの発表では逆に型システムがきちんと考えられていることを窺うことが出来、興味深かった。 最近ちょっとJavaを使っていて、「これはダル過ぎる」と思っていたところなので、Scalaは使ってみたいなぁ。

帰りの電車で、宮本さんのA Scala Tutorial for Java programmers(和訳,PDF)を読んだ。

関連リンク

• The Scala Programming Language
• 2008-05-11 - Onion開発停滞日記

メモ

「/」が foldl とか、「これは酷い」と思ったw

「_+_」といった書き方はOBJ系の言語や、Agda2でも採用されている(Agda2 - ヒビルテ (2007-12-01))ので違和感なし。

……と思ったが、OBJ系言語やAgda2のやつが演算子を関数として扱うための記法なのに対して、Scalaのは任意の式に穴を空けられるのか。 そうすると、例えば _+_.toInt は ((x, y) => x+y).toInt ではなく (x, y) => x+y.toInt と解釈されるが、ラムダ式のボディになる範囲はどうやって決まるのだろうか?　「違和感なし」と書いたけど、前言撤回。やっぱり気持ち悪いかも。

「var z :Array[T] forSome { type T } = x」のとき、z(0) の型は T for Some { type T } ではなく、AnyRef になる。

水島さんのtwitterで取り上げられている implicit parameter の話は、Agda1だとimplicitな引数を明示的に与えるときには、通常の関数適用の f x とは別の f |x という記法を使うことで曖昧性を無くしていたので、Scalaだとどうしてるのかなと思って聞いてみたのでした。

• <URL:http://twitter.com/kmizu/statuses/808199043>
• <URL:http://twitter.com/kmizu/statuses/808199622>
• <URL:http://twitter.com/kmizu/statuses/808200187>
• <URL:http://twitter.com/kmizu/statuses/808200567>

implicit parameter を使った Poor Man's Type Classes 。 そういえば、Agda1での型クラスの実装も内部的にはimplicit parameterを使う形になっていた(“Overloading in Agda” by Catarina Coquand - ヒビルテ (2005-10-03))。

A Nominal Theory of Objects with Dependent Types

λ. RubyKaigi2008と懇親会のチケットを購入

λ. 第五十二回圏論勉強会

今日は圏論勉強会。 写真