https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #ICFP 要塞型マクロ：Schemeのマクロは非常に良いのだが、使い間違った時のエラーメッセージが（手で頑張ってエラーチェックするマクロを書かない限り）マクロで変換された後の構文に従って出てくるので、酷いことになる。これをなんとかする。syntax-parseというので(続 | |
| #ICFP 続)パターン定義すると、するときに、(x:expr y:identifier) みたいにどんな構文要素が来るか定義できてそれに違反してたらそれに応じてエラーメッセージ出せる感じ。なんだか静的型付き言語にあるマクロみたいな感じだ。 | |
| #ICFP Purely Functional Parallel Algorithm：体調悪いので寝てたせいで最後の質疑応答しか聞けなかった…。タイトルの通りの内容。"purely functiona algorithmはsequentialよりもparallelで輝く"(続 | |
| #ICFP 続)発表聞いてないので詳細分かりませんが"programming-based cost model"というのがポイントらしい。machine-based cost modelと比べて。これはなんだろう後で調べる。 | |
| #ICFP Sparse Matrix Code：疎行列の表現方式が"正しく"行列を表現しているかが検証できる、疎行列エンコーダ/デコーダ構築のためのコンビネータDSLを作ったよ、という話。 | |
| #ICFP Shape Polymorphic Matrix： （ ﾟε ﾟ )＜ﾄｩｯﾄｩｯﾄｩｰ | |
| #ICFP （発表者が「行列の掛け算のやり方はみなさんご存じですよね。こうです」と言いながら壇上で歌って踊り出した様子を表す） | |
| #ICFP それはどうでもよかった。中身は、ううむ、発表聞いただけだとExpression Template実装の行列ライブラリとの違いがちょっとわからなかった。論文みたらBlitzと比較してこれよりももっとflexibleだと書いてあったので、誰か詳細読んで教えてください | |
| #ICFP 「各ラムダ式に cost」なるほどありがとうございます http://twitter.com/ksknac/status/25892001110 http://twitter.com/chunjp/status/25891577895 | |
| そういえば寝て起きたら王座戦が終わっていた… | |
| @natsutan 例題がつまらないというのはよくないですねえ。僕は(も)Coqのチュートリアルで同じ事を思った http://twitter.com/gusmachine/status/25814497029 | |
| C++er/Boosterの人はRegular,Shape-polymorphic,Parallel Arrays in HaskellとTotal Parser Combinatorsは面白いんじゃないかなーというか誰か読んで解説plz http://www.reddit.com/r/haskell/comments/dji4v/papers_from_icfp_2010/ | |
| #ICFP CertGC： Coq製C(サブセット)コンパイラCompCertを拡張して、GCつきC（サブセット）"GCminor"のコンパイラ作った話。当然GCの正当性証明付き。HaskellからGCminorへの変換器も。検証済GCて既に山程あると思うけど差はどこになるんだろ | |
| @shelarcy どんどん突っ込んでください | |
| #ICFP Total Parser Combinator：無限ループしない左再帰を書けるパーサコンビネータ。肝は「ここはinductive」「ここはcoinductive」みたいにパーサによってどっちのモードか分かれてて混ぜまくれるというシステム。(続 | |
| #ICFP 続)今あるparser combinatorはだいたいinductiveだけどcoinductiveなものを必要なところで混ぜると一見無限ループになりそうなものもcoinductionになってセーフということか。っていうかこれは実装してみないと気分が全くわからん…っ！ | |
| （すごくおおざっぱな注釈）inductive=foldで書いてある（どうやって"入力文字列を処理するか"スタイルで書いてある） vs coinductive=unfoldで書いてある（どうやって"出力の構文木等を作るか"スタイルで書いてある） | |
| ボルチモア水族館、イカがいなかった… | |
| 時間が無かったのでクラゲゾーンをスキップしたのだけど、もしかしたらそこにいたかもしれない… | |
| #ICFP EDSLのインタプリタのPartiaul Evaluation： Idris http://www.cs.st-andrews.ac.uk/~eb/Idris/ というyet another依存型言語が紹介されてる。これのリッチな型システムを活用して色んな安全性を(続 | |
| #ICFP 続)確保したEDSLを書いたら、インタプリタの部分評価でそれを超高速してやるぜ！という話。少なくともトイサンプルではJavaを超えてC並に速くなると言っている。へー。すごい。今度試してみよう。PyPyとかもそうだけど、部分評価＋インタプリタはそろそろ本気で面白いのかも | |
| #ICFP 超ウルトラスーパーcompilation： supercompilationという最適化テクニックがあって、プログラムを変数入りのままコンパイル時に"実行"してみて、変数の値によって分岐するような式が現れて"実行"が止まったら変数の場合分けを挿入して先に進み…(続 | |
| #ICFP 続)ただし一度見た式が再度現れたら再利用とかして適当に止まると中間データが消えたりした最適化コードになってる的そういうもの（適当）。この技を、主にlet式の扱いを工夫することで、停止性チェックの必要性を減ら(無く?)して最適化プロセスを高速化。出るコードの質はトントン | |
| #ICFP A正規形にしてからsupercompilationすると元コードの部分式しか最適化プロセス中に現れないから前に出てきた式を見たら再利用というストラテジで必ず止まる、という理解でいいんかな。 | |
| #ICFP VeriMLの発表死ぬほど面白い | |
| あまり @chunjp さんの実況 http://twitter.com/chunjp/status/25912049643 に付け加えることなど何もないのだけど… | |
| #ICFP CF： MLの式tに対して、「tを実行したら止まって結果の値が条件Pを満たす」と「[t] Pが真」が同値になるような「命題を受け取って命題を返す関数[t]」を作ることができて、これをcharacteristic formulaと言う、というお話。これがあると(続 | |
| #ICFP 続) 1.MLでガリガリとコードを書く 2.characteristic formulaを自動生成 3.それに証明したい命題を食わせる 4.でてきた命題をCoqで頑張って検証 5.砂糖と塩を間違える、というワークフローでMLのプログラム検証ができていいですね、と | |
| #ICFP 全部Coqで一から書くより既存のMLコードを検証できたりするのが嬉しい、のかなあ。OkasakiのPFDS本のデータ構造を半分くらい検証したそうです。CFの定義が、とてもシンプルで言葉の言い換えをしているだけにも見えるんだけど、でもここは簡潔すぎて逆に凄い感が結構ある | |
| #ICFP VeriML：「今回ICFPで何度も話題に出た検証済みコンパイラCompCertのコードをよく見てみよう。実行可能コード：証明、の比率は実に１：１６だ。」「これは"証明"というものが本質的不可避的にプログラムより複雑だからであり、仕方のないことなのか？」「否」 (続 | |
| #ICFP 続) 「別の検証済みコンパイラ[POPL10]を見てみよう」「規模も違うので単純に比較はできないが、こちらは比率は１：４だ」「工夫次第で証明の記述は簡潔になる」「工夫とは？」「二つのソースを見比べると、後者の方が自作tacticを有効活用している」 (続 | |
| #ICFP (注釈) 証明記述言語では、型＝証明したい定理、証明＝プログラムで、「要は指定された型を持つコードを書くこと」＝「証明すること」なのですが、tacticというのは、証明記述言語の対話環境に用意されている補助スクリプトで、打ち込むと証明=プログラム片を生成してくれるもの | |
| #ICFP 続) 「つまり結論はこうだ」「focus less on writing proof scripts，more on writing tactics」「デフォルトの環境で頑張って証明を書くのではなく、domain specific tacticの作成に注力しよう」(続 | |
| #ICFP 続)「では、そんな素晴らしい結論が流行らないのは何故か？」「既存のtactic記述言語がショボいからだ！」というわけで素晴らしいtactic記述言語VeriMLを作ったよ、という話。フルのMLの表現力に命題や証明に対するパターンマッチを入れて型付きtactic作れる。 | |
| #ICFP 「わかってるx=y型の定理を全部集めてunion-findでまとめて必要な等値性証明を作るtactic」とかが例示されてました。とにかく「tactic記述言語を強化することで証明記述を簡略化する方向に行くべきだ」という提案はとても納得がいって非常に面白かった。 | |
| #ICFP Deptype&Parametricity：パラメトリシティ（…日本語のわかりやすい説明が今もしやweb上にないのでは…なんてことだ）を、依存型というかPure Type Systemに対しても証明したという話、だけではないっぽいんだけど発表が(略)すぎてよくわからず | |
| #ICFP A Play on Regexp： 「論文は劇の台本として書かれています http://twitter.com/kinaba/status/22867687828 が、俺がここで一人芝居を始めると思ったら大間違いだ！(意訳)」ということで普通の発表でした… | |
| #ICFP 正規表現の話は、（GlushkovのNFA構築法を参考に）文字列と正規表現を受け取ると「今読んだ文字は正規表現のどの位置でマッチしてる」ってマークを正規表現の各文字に持って、それを毎文字で動かして最後まで行けたらマッチという実装。Haskellでとても綺麗に書けて速い | |
| #ICFP Googleの中でPythonに混ぜてHaskell使ってる話：http://http://code.google.com/p/ganeti/ プロジェクトチームの人だそうだ。偶然だろうけど一昨日の実用例の話もXenだったし、なんかこういう仮想化管理と相性いいんだろか | |
| #ICFP 型クラスProgramming without overwrapping instance： Habit http://hasp.cs.pdx.edu/ に実装されている型クラスの話。要するに、instance ... else .. else ... fail と | |
| #ICFP インスタンスにif-then-else式に順番をつけられるようにしてoverwrapping instanceの曖昧性の問題を無くす。ShanさんOlegさんSimonPJからすごい激しく質問が飛んでいる… | |
| #ICFP fail を入れたり if-then-else を入れることで暗黙に否定が入ることで non-monotonic logic になって下手するとセマンティクスが実は壊滅的におかしくなっていないか、という辺りが争点のようだ | |
| http://favotter.net/status.php?id=25895712681このアイコンがない人は誰だ！と思ったら、めるぽん先生が謎の進化を遂げた果ての姿だった。これは結局なんでこうなってるんですかね | |
| というわけで夕飯＆帰ホテル。ICFP本会議はこれでおしまいで、僕は明日Haskell Symposiumに出てそれで帰ります。その後のHaskell Implementers WorkshopやCUFPのレポートはどなたかのに期待 | |
| CUFPは http://cufp.org/conference/sessions/2010 の2ページ目の"Scaling Scala at Twitter"がやっぱり何と言っても気になる | |
| ボルチモアにはエドガー・アラン・ポーの墓があると聞いて調べてたらひっかかったんだけど http://www.findagrave.com/cgi-bin/fg.cgi?page=gr&GRid=822 findagrave.com なんてサイトがあるのか… | |
| ICFP 2020 では、今回発表された論文のなかから１本が「The Most Influential Paper」として選ばれるわけですが。それがどれになるか今から予測すると面白い気がする | |
| CPDTはこういうスタイル http://twitter.com/yoriyuki/status/25872397959 http://twitter.com/tmiya_/status/25877166251 なのかー。僕としてはこれはどちらかというと大賛成なので読まねばならぬ | |
| 細かくLemmaやModuleに分けるモジュール化やマクロは、プログラムを簡潔にまとめるには足りても証明をまとめるには力が足りてない気がどうもするんですよね。実行可能なプログラムを書くのとは別のやり方をしなきゃいかんのだと思う。 | |
| @yoshihiro503 強力すぎるtacticがあると、入門として使うのに適しているか疑問、というのはありますね。たしかに。最終的にであれば「強力なtacticを使って証明を書くべき」というのは正しいと僕は思うのですが… | |
| Haskell Symposium のハッシュタグなんだろ。どうせ僕のポスト拾われないから関係ないのだけど…。36 submissions 14 accepts。MLやWGPよりだいぶcompetitiveな感じだ。 | |
| #HaskellSymp パーサとプリティプリンタを同時に兼ねるコンビネータの話： C++でいうとSpirit.(Qi|Karma)が融合されて一個の文法定義で両方できる感じ、というかKarmaを見た瞬間、融合されてないのが不満で仕方無かったのでこれは非常に素晴らしい (続 | |
| #HaskellSymp 続)全体的にストレートに全コンビネータを両方向化しただけのようだ（一点unusualなのが、構文木コンストラクタのparse＆printを生成するのにTHを使用、程度）。どこかにナイーブにやるとハマる罠がありそうなトピックに聞こえるんだけど平気なんかな… | |
| #HaskellSymp 論文リスト http://www.reddit.com/r/haskell/comments/dkzn4/papers_from_the_haskell_symposium_2010/ | |
| #HaskellSymp Haskell標準のコンテナライブラリをベンチマークして遅いとこ見つけて速くしたよという話：質問も出てたけど、ベンチマークの仕方がeagerにfull評価するというのは結構疑問なんだけど大丈夫なんだろか。遅延評価を巧く使ってる部分が過小評価されないか | |
| #Haskell 原始的なLazy関数型言語STG(Shared Term Graph, GHCの内部表現で使われる)から抽象機械STGマシンを系統的に導出する、Coqで：(cps変換+継続のdefunctionalization)(評価器)=抽象機械 [Danvy] へー | |
| @gusmachine これって調べようと思って調べてないんですが、逆に、現れる型のサイズが小さければ時間も小さいんでしょうか。つまり入力式のサイズsと現れる型のmaxのサイズtについてs+tで計算量を評価すると指数ではなくO(poly(s+t))になったりするんでしょか |