https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #ICFP "魔法/【レビテト】FF4から登場する補助魔法で、術者が空中浮揚する"：依存型では、"値を受け取って型を返す関数"を書くことができるので、全ての型をその形で書いておけば、型の記述(Desc)が値として手に入る、つまりreflectiveなプログラミングが自由自在！… | |
| #ICFP …というデザパタをさらに１歩推し進めて、これまでは唯一必要だった型、型の記述であることを表す型Desc自身をも、自分を定義しながら自己記述する形で書けるように整理した型システム、というお話。これにて型記述に一切の土台は不要となり、型記述フレームワークは空中に浮遊する。 | |
| #ICFP これは「Datatype Generic Prog.は依存型さえあれば自在にできる」という論文だけど、今年は他に「Security Typeは依存型(略)出来る」「様相論理や線形論理など部分構造論理は高階論理に埋めてtwelf等の依存型で扱える」とかそういうのが多い | |
| #ICFP 型記述が値となることで、「list なんて nat にパラメタが増えただけでしょ？」「listのconcatなんてnatの加算と構造として同じでしょ？」みたいにnatからlistの全てを導出するようなデザインができないか、というfuture workが面白そげでした | |
| #ICFP "魔神さん http://jp.akinator.com/ を見習って単純型付きλ計算のプログラム当てゲームを作るよ(意訳)"：応用としては、この質問ゲームのyes/noの列を1/0列として使えばビットエンコーダ/デコーダになる。Proof Carrying Code | |
| #ICFP での証明埋め込みとかに使える。技術的な問題としては、「無駄な質問を一切しない魔神さんを作る」のが形無しλなら簡単でも型付きλでは難しい。型の制約があるせいで「判定がPSPACE完全な一見ありそうだけど実は無い可能性」があるため。これをどうにかしたそうな。 | |
| #ICFP 質疑応答で「0/1じゃなくて算術符号みたいに実数重み質問とかに拡張できないか？」「そのビット列はかなりλ式の構造そのまんまな気がするがビット列のままβ簡約とかできないか」といった議論が出ていた | |
| １トーク１ポストに簡潔にまとめようと思っていたはずなのに長すぎるぞ俺… | |
| 論文タイトル書くと長いので省略してますけど http://www.icfpconference.org/icfp2010/program.html この順番でポストしてます。今３つ終わった。 | |
| #ICFP ReCaml：型付き限定継続入りのCamlにラベル構文と「今の継続がここ（とラベベルで指定）ならこう」的なことができるmatch_contという分岐を入れて継続操作を可能にすると、実行時に動的にスタック/コード差し替え等が型安全にできるとか。例見ると使うの相当面倒そ… | |
| #ICFP ロリproc： 古典線形論理からのC-H対応で新しい並列計算言語を作った話。(古典≒継続)を使う側と後の実行を並列にして、間の繋ぎが(線形≒１回)だけ使える、型がdualに合ったチャネルで、セッション型になる。色々デザインチョイスがあるらしいけど細かいとこよくわからず | |
| #ICFP 抽象解釈(参考PDF: http://santos.cis.ksu.edu/schmidt/Escuela03/WSSA/talk1p.pdf ) の系統的な導出法：静的プログラム解析手法の一つに抽象解釈てのがあって、変数の取る値を抽象化して、後はそのままプログラムを"実行"する（例:intを{odd,even}で実行して偶奇性を解析）のですが | |
| #ICFP 抽象化の仕方によって色々な解析ができるそれを系統的に説明する。1:プログラムを普通にメモリの概念があるマシン語にコンパイルする 2:普通の実行は"メモリは無限にある"前提でmallocは常に新鮮なアドレスを返す（実機でできない場合はabort）実行だが | |
| #ICFP 3.抽象解釈実行は、"メモリが有限で、メモリが足りなくなったらmallocは確保済みのメモリにデータを重ね書きする（上書きではなく複数の値を重ね持つメモリセル）"と考えることができる。それだけ。色んな抽象解釈の違いは，単に重ね書きストラテジの違いとしてみられる。 | |
| #ICFP Higher-ranked フロー解析：フロー解析（プログラム中の各変数に、どこで作られた値が入る可能性があるか、をannotateする解析）を型でやる話。面白いのが、higher-rankの多相型（多相型関数を受け取る関数etc）の型推論は決定不能なんだけど | |
| #ICFP どこで作られた値かの注釈に関する∀(forall)量化は、いくらhigher-rankに重ねても推論が決定可能だそうだ。へー。アルゴリズムも有名な型推論アルゴリズムのWとだいたい同じで、"principal type"が求まる。 | |
| #ICFP Reduceron http://www.cs.york.ac.uk/fp/reduceron/ ：FPGAでハスケルマシン作りました！というお話とその細かい工夫色々。Functional Processoer Unit 略してFPUを全てのマシンに！ | |
| #ICFP Xen http://www.xen.org/products/cloudxen.html の話： かなりの部分がOCamlで書かれているプロダクトの例として。 | |
| 申し訳ないがあんまり、○○言語の言語機能や実装の質が「プロダクトレベルで使える」という話に興味が湧かないんだよなあ。全部、当たり前だろ、としか思えないのが…。 | |
| 自分の中では「使える／使えない」＝＝「ライブラリが有る／無い」で、他の条件は別にまあ使うと決まればどうとでもなると思っている節がある | |
| #ICFP LTS：並列化の際に予めデータ分割して各コアでバラ実行、だと良くバランスしないかもゆえLazyにオンデマンドで分割したい、というその好き勝手な分割をrope bit.ly/aPBkZz 用zipper bit.ly/bP4VNf を使って関数的に実現！という話、かな？ | |
| ちょっと無理に140文字におさめようとtwitゴルフしすぎた感がある。 | |
| #ICFP MSの人。M言語ベースのさらに研究用言語Dminor( http://research.microsoft.com/en-us/projects/dminor/ )の静的型検査の話：型に、pureな任意の式や、{x where x in T & x<=100}みたいな論理式制約を書けるので大変である。→ SMTソルバ(Z3)で解く | |
| #ICFP (続) 型チェックは実行時にもできるし、emptyでない型の場合は型チェックのついでにその住民を計算も出来るので、制約を満たす値をみつける制約ソルバのプロトタイプとして便利だよ！というハックが紹介されてて面白そうだった。あとで遊ぶ | |
| #ICFP Racket (旧PLT Scheme) の「動的言語にあとから突っ込む型システム」の話。問題はsymbol?やpair?など、型を問う述語で分岐するケース。こいつらからは論理式を生成して型システムに取り込んで解く。Dminorより表現力は低いが高階関数も行ける。 | |
| #ICFP "Existing programs are a source of type system ideas." ＞Racketのコードベースで使われているこんなidiomが以前の追加型チェッカでは通らなかったが今回の研究なら通せる、という話をしつながら。 | |
| #ICFP しかしPLTの人はいつ見てもこのstring?とかの型チェックをやってる気がするのだけど、古いの覚えてないんだけど、結局どの部分が新しいのだろか | |
| Toward.Boost.countertree http://thread.gmane.org/gmane.comp.lib.boost.devel/208991 これ結構欲しいな。http://twitter.com/cpp_akira/status/17938019147 とかで出てたO(log n)でランダムアクセスできるset/map | |
| #ICFP PC Chair Report：238 attendees. 99 submissions 33 accepts (Us > Uk >> Fr, De >> Jp, Nl, Au, Dk …). 14 submissions had mechanized proof. | |
| #ICFP http://www.reddit.com/r/haskell/comments/dji4v/papers_from_icfp_2010/ 全論文が著者のページで公開されているらしい。みんな読むとよいよ。 | |
| Conal Elliott のメモ化シリーズが面白すぎるのですが…多相関数のメモ化、UNmemoization、Yoneda lemma http://conal.net/blog/posts/memoizing-polymorphic-functions-via-unmemoization/ | |
| #ICFP TeachScheme： Felleisenの、プログラミング教育の話。"デザインレシピ"の話などなど（この辺りの話はOCaml Meetingとかで浅井先生が日本語で噛み砕いてお話しされていたのがわかりやすかった…のは動画とかは残ってないんでしたっけ）。(続 | |
| #ICFP 続)functional vs imperativeで関数型を推すというよりは、inductive(cons-list) vs indexed(array)でinductiveを推しているのだ、そっちの方が教育的でわかりやすく良いデザインにガイドしやすい、と | |
| #ICFP 続)最初っから、常にテストのカバレッジを表示してカバーされてない行は真っ赤になるような環境でコード書かせるのは必須、というのはそうだなあと思う。 |