ICFP そのものについて
完全にド素人なわけで、どうせほとんど何言ってるかわからんのだろうなぁと思ってたんですが、意外とわかるものももあったので書いておこうかと。わかると言っても、どうやってやったかとかまではなかなかわからんくて、モチベーションくらいがわかればそれだけでも嬉しいという幸せな話でして。
プロシーディングはここにあるみたいだ。
以下、たぶん間違ってたりそんなことは重要なことではないということを書いてたりします。
Organizing Functional Code for Parallel Execution
Guy Steele 。面白かった。 car, cdr, cons を使うスタイルは並列化できないからダメで、 item, list, split, conc が適切なプリミティブですよというような。シーケンシャルな方式だと効率悪そうなこともやるのがこれからの常識、的な。このスライドを水増しした感じだったのかな。
http://groups.csail.mit.edu/mac/users/gjs/6.945/readings/MITApril2009Steele.pdf
Functional Pearl: La Tour D'Hanoi
ハノイの塔の状態をグラフにすると大変綺麗でわかりやすい、というような。これの2ページ目の絵は一見の価値はあるかも。
Pearl というのは面白アルゴリズムとか綺麗なものを紹介するコーナーらしい。このへんでなんか意外と色々あるんだなぁ…と思いました。
Purely Functional Lazy Non-deterministic Programming
そもそも Non-deterministic の定義がわかってない。ここでなるほど想像していた ICFP の雰囲気だ! と思った。
A Functional I/O System or, Fun for Freshman Kids
イベントドリブンで関数を登録してやったらいい感じにすれば、ゲームが作れて、子供たちに関数型言語がバカ受け、というような教育話。メッセージを受けるのもイベントドリブンな感じにすれば、自然とサーバー/クライアントなプログラムにも拡張できますよというような。なんかでも例えば timer とかだと、 World -> World とかが関数のプロトタイプみたいだけど、論文のコード見るとその World に set-dx とかしてて、副作用ある感じなのかなぁ…なんか副作用がどうこうは喋ってた気もするけど忘れた。
Runtime Support for Multicore Haskell
なにしたかしらんけど、 Parallel Haskell は使いものになるようになったよ! とか言ってたように思う。
これに限らず並列化系の話題では、「このデータ並列に扱えまっせー」と伝えておいたらタスク(Haskell では spark?)キューみたいなのがよろしく並列でやってくれる、っていう方向性でやってるんだなぁというイメージだった。たしかに Mutex を直に使いたくないしタスクキューみたいなのがあれば便利なのはその通りなんだけど、うーんでも本当に難しいのは全然違うスレッドが協調動作してる時かなぁ。
で、そのへんはコミュニケーションベースでほげほげーとか言ってる人が結構いたように思う。
Experience Report: seL4: Formally Verifying a High-Performance Microkernel
普通は抽象的な仕様があって、その仕様をどう満たすかという実装についての仕様があって、実際の実装があって、それぞれがちゃんと対応してるかをソフトウェアで調べて verification とする、と。
今回は Haskell で microkernel のプロトタイプを書いて、ただそこからバイナリ作ると遅くなっちゃうから本番は C で書きました、と。でも Haskell の prototype から実装についての仕様を生成して、それと C コードの verification をしました。
という話だったんだと、思う。ちゃうかも。
Scribble: Closing the Book on Ad Hoc Documentation Tools
コード中にドキュメント書く javadoc 的なアレで、ただその javadoc が走ってるのも別のツールってわけじゃなくてその言語自身みたいな話だったんじゃないかと。 runtime execution 、 compile time execution に加えて document reading time execution があるとかそういうこと言ってたのが印象的だった。
いやもっと印象的だったのは例えに使われていたお姫様だった。ある日お姫様は1つだけ願いがかなう井戸だかなんだかを見つけて、ステキなお城をもらいました。2人目のお姫様は同じものを見つけて、ひゃくまん個願いをかなえてもらえるように頼んでから幸せに暮らしました。3人目のお姫様も同じものを見つけて、そこら中に願いがかなう井戸があるお城をもらいました。というような。しかしその例えがうまくマッチしてるのかよくわからんかった。
Finding Race Condition in Erlang with QuickCheck and PULSE
Erlang ってメッセージ送る時以外に外部に作用が起きる時は無いので、そのメッセージほるのを hook してユーザー空間(この場合は Erlang VM 外という意味で)のスケジューラに一旦投げるようにしてやって、ユーザーレベルのスケジューラはその他のプロセスを完全にシリアライズしつつ、一個ずつ適当なプロセスを起こしてメッセージを投げるまで待って…をしてやる、と。でまぁそのユーザー空間で動いてるスケジューラはログを記録して race condition を再現してやれます、という話。
メッセージの hook は Erlang のソースのトランスレートみたいなのをする感じでやったみたいだ。たぶん。
あとはなんか知らんけど、 race condition を起こすコードを自動生成して、かつ見つかったら適当な試行錯誤でそのコードを最小化してくれる仕組みがあるらしい。へえ…
race condition を起こすコードを自動生成できる理由は、要は全ての関数が atomic だと仮定してるからっぽい。全ての関数を順番に実行してみた時の結果と、適当なスケジューラがほげほげした時の結果が違ったらアウト、と。
全体の中で大変興味深い話の一つだった。 linux kernel とかも scheduler にちょっとこのプロセスの thread の動作記録しといてちょ、とかできるといいなぁ。 valgrind とかだと遅いのが結構致命的なんだよなぁ…てか既にあったりしそう。
Partial Memoization of Concurrency and Communication
面白そうなタイトルなのになんのこっちゃだったので印象にのこった。
Experience Report: Haskell in the "Real World": writing a commercial application in a lazy functional lanuage
日本で Haskell で仕事するとか D 並に猛者だなーと思った。 Haskell の型検査通れば大部分のテストは書かなくていいという話が、少し違和感を感じたかも。ユニットテストって確かに書くのめんどくさいんだけど、書いてしまえばちょっとした API のサンプルにもなるし、書いてる最中に API の設計が悪いとか気付けたりする副次効果もあるので、めんどくさいけどいろいろ悪くないものではあるんだよなぁと。まぁでもその代わりにドキュメント書けばいいだけの話という話もある。
なんか ujihisa さんが読んでるな。
http://ujihisa.blogspot.com/2009/09/summary-haskell-in-real-world.html
Beautiful differentiation
ハノイの Pearl に比べて圧倒的に難解というかほぼ何もわからなかった。たぶん微分方程式は解析的に解けない場合もあるし、数値解は数学的な特徴がわからんくなるので、間のアプローチとして高階関数 d を作れるという話だったんだと思うんだけど。
OXenstored: an efficient hierarchical and transactional database using functional programming with reference cell comparisons
Xen のマネージメントツール的なものを transaction のアルゴリズム見直して OCaml で書き直したら速くなった! みたいな話だったと思う。 DB の transaction がどうこうは結局何がどういうシーンで良いのかよくわかっていない。ベンチマークでは数が増えない段階でもオリジナルの C のより速くなってるんだけど、まぁこれはオリジナルがへちょかった面が強いんじゃ…
なんか ICFP こいうのもあるんだなー的なのの一つか。
Identifying query incompatibilities with evolving XML schemas
世の標準規格は、アップデート時に既存の XPath とかが壊れないことを証明せずにやってる、けしからんから俺が検証器作った、という話。現に MathML 1.0 から 2.0 へのアップデートでの非互換性を発見したらしい。
質問で w3c と話したのかとかいう話があって、実際こういうのはありがたいんじゃないかなぁと思った。
Experience report: ocsigen, a web programming framework
Webサーバとその他もろもろを OCaml で作った的話。 OCaml VM を JS で実装したみたいな O'Browser が面白そうなので終わった後話聞いてみた。 Hot Ruby について聞いたような問題がまさに起きるっぽい。要は asynchronous にするの大変でかつ遅くなるというような。 OCaml をコンパイルする ocamljs というのもあるんだなぁと学んだ。
Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
Scala に部分継続を入れたよ! あんま遅くならんかった! という話。
そもそも部分継続ってなんだろーくらいの勢いだったので、後でそのへん研究されてるという日本の方にお聞きしてみた。完全なヤツだとどうしようもなく全部 CPS 変換せにゃならんけど、部分継続なら影響あるところだけ CPS 変換すればいいんだよーという理解であってそうな。
継続とかは一度ちゃんと勉強した方がいいなぁ。
A theory of typed coercions and its applications
Coercion の型安全というのは話としては面白そうなのだけど、何言ってるかよくわからんかった。 Microsoft research の人は総じてむつかしかった気がする。
