ESOP 2009適当実況（一部）

ESOPに来ています。European Symposium on Programming（プログラミングに関する欧州会議）の略で、POPLのヨーロッパ版?みたいな学会です。プログラムはこちら。日本でのリモート仕事が山積みで、全部は無理なので、ちょっとだけ「適当」（＝いい加減）に実況します。

  • ヨーク大学の寮に泊まっているのだが、ガッガッという鳴き声で起こされて外を見たら、きれいな羽の鴨が道を歩いていた（隣に湖があるから？）。近づいても逃げない。
  • 朝食。目の前にワドラーがいたので、一緒にピッツのいたテーブルへ。ずっと一言もしゃべらない人がいて、一人だけ先に席を立ったので「シャイな人だなー」と思ったら、ちらっと「モッジ」という名札が。ワドラーに聞いたら「あれ、会ったことないの？　だったら紹介したのに。確かにシャイで、みんなでモナドの話をしてても黙ってたりするけど」みたいなことを言われた。
  • あと、ワドラーが「二人とも目の前にいるから聞くけど、論理関係と双模倣ってどう違うの？　どっちが良いの？」みたいなことを言い出して、ピッツが「論理関係は存在すること自体の証明が難しくて、双模倣は合同性の証明が難しい」とか答えていた。アブラムスキーの適用双模倣はそうかもしれないけど俺の環境双模倣は違うYO!っていうか、論理関係の基本補題の証明が環境双模倣の合同性証明とほとんど同様なので嘘じゃないかと思ったが、朝食でそこまで必死に反論するのもどうかと思い空気を読んで自重。先週のコペンハーゲンでの議論でfree theoremも扱えることがわかったし、後でまとめてメールするかした（←全然自重してない）
  • 予稿集の前書きに突っ込んだことが書いてあって楽しい。「LNCSで15ページという制限は馬鹿げている(absurd)」とか「一名のPC memberが、催促してもreviewを提出せずrebuttalに少し遅れた」とか。

The most common, printable, adjective used to described （原文ママ） this limit in the PC discussions was “absurd”

  • Wolfgang Thomas氏の招待講演。後で書く（時間があれば）
  • Session 1
    • Gradual typingとかhybrid typingとかcontractとか（古くはsoft typingとか）、静的型付けと動的型付けを組み合わせて使う話×２。動的型エラーが起きたとき、「誰が悪かった」のか、原因となったコードをピンポイントに特定する"blame"の定式化とか最適化とか。さんざん聞く話なのでわかりやすいが、目新しいところがないような…
      • ワドラーが手に絵を描いてパフォーマンスをしていたが暗くてほとんど見えず
      • [Q by フェライゼン（隣にフィンドラー） to 2番目の発表] ハーパーは型無し（＝動的型付き）言語は（再帰型のある）静的型付き言語のsubsetだと言っているが、Church-Turing thesisを超えて考えれば実用では云々 [A] この研究／論文ではout of scope!
    • Typed Schemeでの可変長引数の型付け。複数引数のmap
(map (lambda (x y) (cons y x)) '(1 2 3) '(a b c)) ⇒ ((a . 1) (b . 2) (c . 3))

とか。HaskellやScalaでは「引数9個まで」とかad hocにoverloadしている。ここでは

∀ (R A B ...) ((A B ... → R) (List A) (List B) ... → (List R))

みたいな型を与える（「...」も正式なsyntaxの一部）。複数引数のmapを使ったfold-leftとかを定義してもちゃんと型付けできる。たくさん「...」があるときは、どの「...」なのか、その...を含む型変数列の先頭の型変数を添えて区別する。実際のPLT Schemeのコードベース（60万行）で5〜10%は何らかの形で可変長引数を使っている（可変長引数関数の定義または呼び出し）。

      • [Q] Polytypic programmingでできるのでは？ [A] よく知らない
    • αMLの話。α変換とかが組み込まれた、言語処理系実装用の関数型＆論理型言語。λPrologとかFreshMLとかαPrologの親戚。これもまたか、という気がするが、どこが新しいんだろう…（右にピッツが座っているが、さすがに「どこが新しいの？」とか聞けない）
      • [Q by フェライゼン] 型がなくても同じことできる？ [A] 現在は簡約で型を使ってるところもあるけど、多分可能
  • 昼食。ピーター・ティーマン（シーマン？）によるとICFP 2011は日本でやるらしい（2010はアメリカ）。あと、センサーネットワーク用のDSLを作っていて、CPSとVHDLの両方に詳しい学生を欲しているらしいので「東大ISのカリキュラムならVHDLでCPU作って、そのCPU用のMLコンパイラ作るけど、ドイツ語は話せないと思う」とか言ったら「ちょうど日本語を勉強中なんだけど」とか言われた。
  • レイノルズの招待講演。準備が間に合わなくて急遽内容変更(!)。「アノテーションつき仕様」から「証明」を導く話らしい。今のところは普通の公理的意味論とかseparation logicとかの話ずっと公理的意味論とseparation logicのターン。公理的意味論は高階関数を扱えないのが難点だと思ったが、案の定、"procedure"（関数）のところで"simple procedure"（簡単な一階の関数）に限定している。公理的意味論の推論規則ばかり40分ぐらい続いていて、会場が飽きているような…（現在進行中）終了。
    • 正直、講演は誰でも知ってる内容だった（と思う）ので、当然の結果として質問はより最近？の問題に集中（並行プログラムの検証とか）。
    • レイノルズ、レーザーポインタでスクリーンではなくノートPCのほうを指す（笑）
  • Session 2
    • 会場が離れているのに休憩時間がなくて遅れた
    • ので一つ目のtalkは聞いていない
    • 二つ目のtalk：いろいろな副作用を表す新しい枠組み？らしいが、CCSのparallel compositionやinput/outputのpipeもあらわせない？そうなのでショボいような…
  • Session 3
    • Java (nominal subtyping)の実際のコードベース(Apache Collections, SWT, ...)をstructural subtypingで解析（型指定とは無関係に型推論）して、無駄や改善の余地がないか検証。ライブラリとかObject, String, int等以外では、94%が不必要にspecificな型指定（structural typeのほうがインターフェースよりmore general）。しかし91%は対応するインターフェースが存在しない。同じstructural typeが繰り返し出現する場合も多数なので名前をつけるべき。実際に目で見ても意味のあるstructural typeがたくさん。しかし、すべてインターフェースとして定義すると数が多すぎるし、nominal subtypingでは既存のインターフェースの「上」に後からmore generalなインターフェース(superinterface)を追加することはできない。よってstructural subtypingが必要、と結論。実際、適切なインターフェースが存在しないせいで、実装(implements)していながら常に例外(OperationNotSupported)を投げるメソッドもたくさん。適切なsuperinterfaceがないせいでコードのコピペが発生することもしばしば（Eclipse JDTで44箇所、等々）。
    • Javaのgenericsの型引数のvariance（+とか-とか）を型推論する話。
    • Ownership typeのvarianceをexistential typeで表す話？？
  • 鉄道博物館で晩餐会。といってもイギリスなので料理の味は（略）。０系新幹線が展示されていました。