に参加しました。感想や説明の補足、発表資料などはすべてこの日付のログにつけることにします。今週以降、時間をかけてのんびり追加する予定です。よろしくお願いします。内容の濃い話を沢山聞けたので、整理する必要があります。主催してくださったいなばさん、会場を提供してくださったサイボウズ・ラボ様、ありがとうございました。
[2009-04-28:追記]428の日にようやく下書きを清書することができました。ふいー。
_ 型レベルプログラミングの会 予告(注:2009-04-18に行われ、無事楽しく終了しました)
<![CDATA[
申し訳ありませんが、ここには SWF (Adobe Systems Flash) が置いてあります。お見せすることができなくてすみません。
]]>
ustream配信あるそうです。発表プログラムは、型レベルプログラミングの会のページをご確認下さい。
みんなも Wii の セガ・チュンソフトプロジェクト | 428 〜封鎖された渋谷で〜を遊ぼう！この、セガ・チュンプロジェクトのサイトにあるムービーデモを見れば、だいたいどんなゲームかわかります。
すっかり近野さんのファンになってしまいましたよ。特典付きを買ったので、メイキングDVDがついてきました。それで、ついカッとなって私もパロディを作ってしまった。偉い人に怒られはしないかと、今は後悔している。
_ 発表資料(“４２８メソッド”)
自動再生されないので、SWFプレイヤーで再生を開始してください。最初のフレームは真っ黒です。異常ではありません。予告トレイラー、発表資料ともに、4:3 のサイズに変更しておきました。そうしておくと世の中いろいろと便利らしいです。
しかし、こちらは予告トレイラーよりもますます偉い人に怒られそうな内容です。４２８の売り上げが再び上がってくれて、許してもらうことをお願いする次第です。
わたしは映像についてはまったくの素人ですが、ネーム・絵コンテからはじめて、構図や人物ポーズ、その他もろもろを準備した上で臨みました。力入れるところが、完全に斜め上で間違ってますね。そういう、小ネタというか、どうやって作ったかみたいなのも、自分のために文章化しておこうと思います。
<![CDATA[
申し訳ありませんが、ここには SWF (Adobe Systems Flash) が置いてあります。お見せすることができなくてすみません。
]]>
_ 二十一世紀ひのまる動画、略して二○動用リソース
ぼくはなんだかよくわからないのですが、まとめ wiki のエンコード設定を参考に、.mp4 に変換してみたので置いておきます。これをあれこれすることについて、僕に断る必要はまったくないですが、セガ・チュンソフトさんのことは頭においてください。
二○動はアカウント持ってないんです。ホントーです。ぼくは面白いものをみつけると、ずーっと見てしまう人なので。前にもそんなこと、ここで書いた気がする。
一方で、『ハックス！(1巻)
』の主人公のとあるセリフは、今回のスライド作りならびに予告トレイラー作りへの衝動をかきたてるに十分だったので、ここに紹介しておきます。二十一世紀ほにゃららもハックス！に出てきます。
- みよし
-
アニメ作りませんか！
たぶん みんなで アニメ作ったら すごい面白いです
アニメのすごい… すごい！っていう エネルギーを使って アニメを作るんです！
[ハックス！第一巻 Cut 2. 「スイッチオン」53 ページより引用]
皆さんの発表がまとまってます。いなばさんも忙しいひとなので、のんびり更新待ってます。更新しなくても、別の人がまとめてたら、そこ参照するようにします。
私の発表は、ustream.tv に録画されています。
- 02:01:42 あたりから 02:21:26 あたりまで : 発表
- 02:21:26 あたりから 02:33:55 あたりまで : 質疑応答
聞こえにくい部分もあったかもしれないので、あとでテキストとしてここに書き残す予定。あと、一次会、二次会で特記しておくことがなんかあったらそれも。[2009-04-28:追記しました]
_ 型レベルプログラミングの会・依存型(HaskellとAgda2で)
映し出される前の、ぼそぼそとした独り言が私のメッセージです。残りのスライドはおまけです。ustream でよく聞こえていないので、ここに台本おいときます。02:02:49-02:04:49 の、「2分」で言いたいことは言い終えていました。
- わたし
-
で、えっと、じゃあ、あの、ちょっと接続に時間がかかっているんで、あの、喋りながらやりますけど、えっと、型レベルプログラミングとは何か、って僕ずっと考えて、えー、ま、そんなに考えていないんですけど、ずっと考えて、結局、型レベルプログラミングっていうのは first class が型なんだと。つまり、普通のプログラミング言語では first, first object は値なので、えーと動かしてみて決まって、えーとあの、それが動的に、あれ、どうしよう、決まるんだけど、型レベルでやれば、コンパイル時にわかるから、だからいろんなことが省けて、で、コンパイル時にバグが取り除ける。
要するに、コンパイル時に、打ち間違い、さっきの(いなばさんの発表)、uとvの打ち間違い、みたいなバグを取り除きたいということがやりたいわけですけど、それを究極的にやるとどうなるかっていうわけですけど、引数を持つ型とか、型の型とか、型の型の型とか、あー、もうどんどんあがっていくわけですけど、やれることが増えていくわけです。
で、そういうことを、まあ、いろんな人が考えていて、ひとつは、依存型、ですけど、残念ながら、依存型は、絶望的です。ということで、トレードオフが必要で、まー、いままでみなさんが、たとえば Scala とか D とか、ま Haskell はいずれ勝手に絶望するんですけど、手続き型言語でトレードオフを取るのが現実解。
僕の話は、理想を追い詰めてしまったがために、絶望する、そういう話です。(以下略)
静的型付け関数型言語好きなひとにはおなじみの、「型安全」の枠組みは、所詮は箱庭(λ-cube)にすぎなくて、できることには限界(Girard's paradox)がある。んだけど、そーゆー話を C++ とかに興味がある人の前で喋ってもすべるだけなので、私の発表は全力疾走で斜め上を駆け抜けました。
とはいえ、発表枠の中では、Conor McBride, "Faking it - Simulating depending types in Haskell", Journal of Functional Programming, Vol. 12, Issue 5, pp. 375--392, July, 2002.の中に現れる、「有限長のベクトル」を紹介しました。この具体例は、他の人のプレゼン(Scala, C++, Haskell, D, G'caml)のすべてに現れていて、見ている人にはよい比較になったのではないかと思います(私除く、スライド早すぎて見えないので)。
依存型や Haskell が絶望する、というのは、一見、他のプログラミング言語よりも凄いことができそうにみえますが、今回の型レベルプログラミングの会でわかったように、他の静的型検査でも faking it できるわけです。
じゃあどこに違いはあるのか、というと、Haskell や依存型プログラミングが小難しい型理論を背景にしている割には、肝心のところに手が届かない。結論：「プログラムを書く人は賢くなければならない←それって、最初の出発点(プログラマがうっかりバグを書いてしまうのを防ぎたい)に戻っているじゃないか」「理想を追い求めると、型検査が停止しない(一階述語論理のクラスが決定不能、に帰着)」「実行速度が遅い、空間計算量が大きい」→動的言語＋テスト網羅で、あきらめるのがいいよね。ああ、絶望した！机上の空論だったことに絶望した！！もう圏論なんか知らない！
とかいうふうな結論を勝手につけるわけです。(つづく)
_ 型レベルプログラミングの会・依存型の質疑応答(の聞こえにくかった最初だけ、テキストに)
質疑応答の部分は、ustream 02:21:30-02:33:52.
- 証明の自動化
-
例として、SAT solver に代行させるというのを挙げました。他には、Coq の auto. tactics や omega. tactics。Isabelle/HOL のいくつかの自動証明ツールが非常に強力です。CSP prover についても何か言えばよかったな、すみません。
いっぽう Agda 2.2 にはありません。Agda 1 (prototype) の Fredrik & Martin の auto prover はどこへいってしまったのだろうか...
Fredrik Lindblad and Marcin Benke. A tool for automated theorem prov-
ing in agda. In TYPES 2004, volume 3839 of Lecture Notes in Computer
Science, pages 154–169. Springer, 2006
Fredrik も Marcin も非常に好人物で、Chalmers 滞在時はお世話になったのだが、今調べると二人とも Chalmers にいなさそうだという...うぐう。
Agda2 の Haskell FFI 以降の話は、さかいさんとの私的な会話だね、と勝手に決めつけ。あと他にも諸々の質問が出ましたが、スライドと一緒にしないとテキストに落とせなかったので、残念。
- 証明できないものの取り扱い
-
みんなで絶望しよう！(エンドカード)
_ 型レベルプログラミングの会：一次会の記憶
会場までは ranha さんと一緒だった。感想をどこかに書いてくれていたけど、ここだけの話はここだけにしてくれて助かった。ぎりぎりパーで、もう少しでボギーです。
アキラさんに「C++ってバランスのとれたいい言語ですね」と言った。私がかわいいと思っているのは C だったり Objective-C だったりするんだけど、これらはあまりにもキャストで proxy なので、ほどほどにがんばってる C++ がいいとおもう。
ぱきらぽんの人は日本の狭い世界を知りすぎているので気をつけてください(もう脱出したのかな)。僕は町田で接待してクチ止めしなくてはならないと固く心に誓った。
びくびくするのももうすぐで、苦界から脱出してしまえばこっちのものだ、フフフ。
_ 型レベルプログラミングの会：二次会の記憶
さかいさんと二人でしんみりとした話をしんみりとする。など。途中でいなばさんが来てくれたので、プログラミングは楽しいですよねーとか、問題を解決するアルゴリズムを考え抜くのがいいんですよねーとか、そういう普通の話をした。めでたし。
は、買いました。
は買いました。
