なごや2013(夏)まとめ
8/25,26でなにやらイベントが連続していたので行ってきました。
後続のせいでかなり地味な印象になってしまったけど(^^、聴いて意味があったのは前半。
OCamlSummit
期待していた Generic Pretty Printer は改造letでデバッグログを吐くお話で、通常camlp5では得られない型付きASTを得るために二段階コンパイル(後段は純正コンパイラ)で実装しているようです。
OCamlではcamlp5/4が使えるので、この手の問題に対してはあまり縛りプレイはしなくて済む感じですね。うらやましい。
他にはherokuというのが簡単に何か出来そうだなという印象でした。
ProofSummit
ProofSummitはほぼCoq(=SSReflect)でした。id:pi8027 さんが何言ってるのか分からないのは私にとってはデフォ。
SSReflectは数学に便利なtacticのそろったライブラリのようですね。とりあえずインストールくらいはしておこう。
あと面白かったのは可逆読み書き器で、書き出して読むと元に戻る証明付きPEGのパーサ/プリンタコンビネータがCoqで出来てました。
仕様の合成は自動で出来るけど、人手で綺麗にしつつやってくと証明し易くてよいみたい。
この実装自体は一般的な可逆計算ライブラリの上に構築したとのことだけど、可逆計算？もとに戻せる計算縛りの数学分野があるんでしょうかね。
あとはCoqたんにはβ簡約が必須というレギュレーションを知りました。気をつけたいです。(何を？
なごやまつり
ヒドイ会でしたね。( ꒪⌓꒪)
こっちではpi8027さんの発表の難易度がかなり控えめで、なんとなく言わんとしてる事は分かったような…きもするような…。
しかしやはりその場で(Goalの)論理式読むのは難しい。
それはともかくLINQPadというソフトが便利そうでした。C#のGUIなREPLみたいです。仕事でC#使うならあるといいかもなという感じ。
発表ではないけど @masterq_teokure さんが運搬してたλカ娘が大変そうだった。お疲れ様でした。とりあえずパーサのとこから読む予定です。
懇親会
ここで初めて話せた/会った人達
- @chunjp さん お昼ご飯でSML#の話をしていたら特定されていた。こわい。あと継続(というか軽量スレッド)の話を振ったら継続の実装方法の論文(へのリンク集)が帰ってきました。わーい(棒)。継続については @dico_leque さんにも教えてもらいました。継続は強力すぎるので限定継続にしとけという感じだったような…？(記憶が曖昧)
- @osiire さん CML本の話を聞きに行ったら、CMLの概観と特徴、実装、Lwtとの比較について教えて頂いた。単にもモナディックにすればよいモノでもなくて、キモは choice : 'a event list -> 'a event による非決定的な選択(?)みたい。
- @yusuke_kokubo さん。ファントムタイプ(株)の人。大して技術っぽい話はしてないのでここに書く事は無いんだけど。ローカルネタとお仕事の話しました。2人以上の単位で動くSIer、ちょっと期待してたりします。
- @maeda_ さん(初対面ではないけど) 幽霊型について話を聞きに行ったらいつのまにか自分が好き勝手話し続けていた…。すいません。
最後に
今回は特に落ち込んだり衝撃的だったりしたことは無く、いくつかTODOが積み上がった気がするので堅実に消化していきたいです。
