https://twitter.com/kinaba のログ (twilog の方が便利です。)
| #WGP C. McBride の招待講演：Typed Term（≒静的型付きDSL）を綺麗に書くには…単にtermと型チェッカを書くのではなく、termの文法定義自体に型整合性がマジカルに埋め込まれているような素敵な書き方で書くには、という楽しい問題があります(続) | |
| #WGP 続)スコープの面倒をマジカルに見るにはNested Type。単純型ならGADTで行ける。では依存型のある埋込DSLを作るには？依存型があればＯＫ！と、まあ実際は事はそう簡単でないのですが、ホスト言語の依存型を上手く掠ってきてそれを綺麗に実現するテクニックの話。面白かた | |
| #WGP Scrap Your Zipper：sybスタイルでgeneric zipperを書いたよという話。この辺の言語機能のチュートリアルとしてわかりやすかった。しかしこう、つい、Dなら一切効率落とさず、もっと型安全で、スキップ指定なども自由な物が書けるよなーとか思ってしまう | |
| #WGP Generic Storage：再帰的な型を定義する時に不動点演算子（Y等）を明示的に貰って使う形で書いとくとアスペクト的に外から機能を注入できる（http://www.kmonos.net/wlog/82.html#_1927080229 )という技を使って、外部ディスクに格納されるデータ構造を作る汎用フレームワーク | |
| #WGP Generic Subexpression：同じく不動点演算子によるアノテートを使って、構文木を表すデータ型に「ソースコード上の位置」の情報を外から埋め込むよというお話。さっきのにもSPJが質問してたけど、まだ"too much is polluted"と感じるなあ | |
| #WGP …parser combinatorやcatamorphismを、位置情報awareにするには手で結局書き換えている辺りが。sybっぽくやって、もっと非侵入的にできるか？perhaps、という議論がなされている | |
| #WGP Q:「コードの位置情報」は、いいんだけど、コードの変形するときに位置情報をどう伝達するか考えるのが一番面倒いところだと思うんだけどそういうのはどうするのだ A:Future Work / ConorがCoMonadでアノテートするといいよ！と言ってるけどよくわからん！ | |
| WGPは [発表] → [事前にassignされた "ディスカッタント" が１人が前に出てきて発表者と議論] → [通常の質疑応答] と３段階の発表構成になってるのが面白い。 | |
| #WGP Generic Multiset：multisetをベタで持つんじゃなくて、∪と×演算を記号的に演算の構文木として持つ＆クエリもできれば構文木で持つと、Genericな同値類分解アルゴリズムで実装を彩れば対multisetのSQL風クエリが超簡潔かつ効率的に言語内で実現 | |
| #WGM (続) ∪と×は記号的だといいよ http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V1G-505NSB3-D&_user=10&_coverDate=08%2F28%2F2010&_rdoc=1&_fmt=high&_orig=search&_origin=search&_sort=d&_docanchor=&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=f71b31464ccbbe45e46ae47a7bef0b9e&searchtype=a てのは前に自分も書いたので納得で、ただ僕の場合は空集合Φは記号的じゃない方がいいと注釈がついたんだけど、それは僕のはsetを構築するまでの話で、これはその後でそれにクエリする話だからという差かな | |
| #WGP DemeterF：関数型界隈でやられてるGeneric Programmingはパターンマッチ＋再帰を汎化してく方向だが、逆にOO的なVisitorから始めて行くという方向でやってみたという話。foldっぽいシグネチャのvisitorを外部ツールで静的自動生成するだけ？ | |
| #WGP CleanのDynamicを型クラス対応にする話：２つの意味があって「単相型やパラメタ多相型に留まらず、型クラスで量化された値Ord a=>[a]->[a]などをDynamicに放り込めるようにする」のと「"Dynamicに入っている型がOrdならソートする"みたいに | |
| #WGP (続)Dynamicに入ってる値の型クラス＆辞書を動的に取り出す」を可能にする。概ねまあそうだよね、という実装をちゃんとした感じ。ただ質問が出てて、型クラスのinstance宣言自体をDynにパックしないので、通信越しに相手に無い型を動的に飛ばすとかできず残念よね、と | |
| #WGP Reason Isomorphically：「米田の補題は楽しいよ！」という話。面白かった＆発表者が凄く楽しそうだった。Haskellの言葉で言うと、「型AとBに一対一対応がつく」ことを証明するには、「∀α.(A→α)→αと∀α.(B→α)→α」の一対一対応を示せばよい | |
| #WGP (続)という方針で、直接両方向の関数を構築するよりも、一段上に上がってから同型性の導出をすると随伴で定義された色々な型を関数のdomainとcodomainの間でいろいろ動かす証明が綺麗に書けるので綺麗、という感じ。論文も読みやすい | |
| #WGP Muさん＆森畑さん：プログラム運算スタイルで効率的なアルゴリズムを導出する際に使う定理の一つにThinning Theoremてのがあって、ある種の枝刈の形式化と思ってるんだけど違うかも的な物ですが、これを"近似解"へと一般化してFPTASの導出に使えるようにしたお話 | |
| WGP http://osl.iu.edu/wgp2010/ はプログラム委員にAndreiがいてG. Brachaがいてdgregorがいて今年は何が始まるんだ…とちょっと期待していたんだけど、結局例年通りのGeneric Haskell方向の論文しか集まらなかったみたいだった | |
| 今日の他のワークショップについては @ksknac さんの #ML2010 実況があったみたい。一昨日のHLPPについては @chunjp さんが後でまとめると言っていたので勝手に期待している。そしてICFP本会議は明日からです。 | |
| #ICFP Milner追悼講演：高校時代から始めて、"How ML Evolved"他60～80年代の文献を見つつMLがなぜこの言語設計になったかを振り返る。「なぜ高階か？」「MLやLCFは元々証明のtactic記述言語として作られたので、X->Yを引数に取るのは必然」(続) | |
| #ICFP (続)「なぜ静的スコープか？」「証明として読んだらそっちが自然」「なぜ型付き？」「証明の正しさの保証」「多相型、型推論？」「型書かなくていいLISPが好きだったから」「参照、破壊的代入」「巨大な証明木の編集を効率的に実現するには必要だった」「例外」 | |
| #ICFP (続)「tacticを適用してみてやっぱりダメでした、というtryを表現するために」「正格評価」「すでに副作用入ってるし、debugの楽さとか」。あと小話として"JACMがSimulationの最初の論文をrejectした形跡があるのだが…??"という追跡が面白かった | |
| （いわずもがなの注釈） Robin Milner さんというのは、関数型言語のMLや並列計算モデルのπ計算を作った人です。今年の３月没： http://en.wikipedia.org/wiki/Robin_Milner | |
| #ICFP ところで僕の横に、車を作ったりその燃料を作ったりするのが上手そうな人々が６人ほど並んでおり、壮観であります。(cf. http://d.hatena.ne.jp/ku-ma-me/20100621/p1) |