How wonderful to be (statically) typed 〜（静的に）型がつくって素晴しい〜 konn-san.com

発表内容の紹介

PFI の全体セミナーで「How wonderful to be (statically) typed 〜（静的に）型が付くってスバラシイ〜」と云うタイトルの発表を行いました。

内容としては、Haskell に限らず、強力な型システムと型推論によってもたらされる記述力と、それを応用した実用的な技術についての解説……の予定でしたが、時間が足らずにHaskell の布教だけで終わってしまいました orz

発表で言及した ¹ 応用例の一覧は下の通りです。

• 型クラスによるデータ操作の抽象化^★
• 静的で型安全なキャスト用クラス^★
• キーの型ごとに最適なデータ構造を自動的に選択^★
• 型エラーが出ないことが静的に保証されている抽象構文木^★
• 高速かつ純粋な破壊的代入を実現する方法^★
• 効率的で外部へのリソース漏れがないことが静的に保証されるリソース制御^★
• リージョン推論によるメモリ確保・解放の自動推論
• 整合性が静的に保証されたスレッド/ネットワーク通信^☆
• 範囲外アクセスを静的に防止するための長さ付きリスト^★
• msgpack の serialize/ deserialize の実装がそれぞれ逆演算になっていることの静的な証明
• 挿入が順序を保つ証明から、挿入ソート函数を自動抽出する手法

これらの技術を説明するために紹介したのが、以下の型機能です。

1. 型とは何か？──型付け、型推論、型安全
2. 強力で wonderful な型システムの紹介
   • 型クラス
   • 型族（関連型）
   • 幽霊型とランク2多相
   • Data Type Promotion
3. 依存型（存在の紹介のみに留まりました……）

本来ならば、依存型と定理証明の辺りももうちょっと詳しく言及して、「Haskell の布教だけじゃなかったでしょ？（ﾄﾞﾔｧ」って云いたかったんですが、いかんせん準備時間がたりませんでした……ぐぬぬ。

反省

• もうちょっと応用に的を絞って、理論背景の説明は省いてもよかった
• Haskell 以外の話題をもう少し入れるべき
  • Haskell とか知らない人向けで書いたつもりが、知らないとけっこう難しかったかもしれない……。
  • 「こんなことができます！」と応用を紹介してから理論背景の説明に入ると盛り上がったかもしれない。
• C++ とか全然わからないのに言及してごめんなさいゆるして……。

参考文献

発表スライドにも載っていますが、参考にした文献を以下に挙げます。

1. ”Fun with type functions“, Oleg Kiselyov, Simon Peyton Jones and Chung-chieh Shan, 2010
   • 開発者向けの型族や関連型の機能紹介と例が豊富に載っています。型族の例の殆んどはこちらから引きました。
2. “Giving Haskell a Promotion”,B. A. Yorgey, S. Weirich, J. Cretin, Simon Peyton Jones and D. Vytiniotis, 2011
   • データ型の、型レベルへの持ち上げ機能（Data Kinds）の紹介論文です。
3. “Lightweight Monadic Regions”, Oleg Kiselyov, Chung-chieh Shan, 2008
   • リージョンによるリソース管理を、phantom type と type-class の機能により実現する話です。例もこちらからひきました。
4. “Region-based resource management”, Oleg Kiselyov, 2011
   • 上のリージョンの実装以外にも、幾つか Haskell の型と Region に関する話題が載っています。Heavy weightな実装とか、動的な演算をトラックするリージョンの話題など。
5. “Algebra of Programming in Agda”, Shin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson, 2009
   • 依存型の機能を使って、証明からアルゴリズムを抽出する話などが載っている、らしいです。らしい、と云うのは読めなかったからで、従って全然紹介出来ませんでした。
6. “Yesod Web Framework for Haskell”
   • 型族の機能をふんだんに用いたモダンなWebフレームワーク Yesod のページです。例が細かくなってしまうので、今回は紹介も説明も出来ませんでした。
7. “データ型 - Wikipedia”, Wikipedia
8. “Type safety - Wikipedia”, Wikipedia
   • うぃきぺ先生はなんでもしってるなー。
9. “Phantom type - HaskellWiki”, HaskellWiki
   • 幽霊型の定義を確認するのに使いました。あってた。よかった。応用例とか色々載ってます。GADTs の話は載ってませんが。
10. “full-sessions-0.6.1”, id:keigoi
    • 作者である keigoi さんによる、セッション型ライブラリの解説です。セッション型、と云うのは、チャンネルを介したスレッドやネットワーク通信が整合的に行われていることを、型で静的に保証する手法です。
11. “プログラミングCoq”, 池渕未来
    • 当初は定理証明についても幾つか言及しようと思っていたので、Coq での証明駆動開発の日本語入門文献として挙げておきました。結果的には殆んど何も云えなかったんですが……。