発表内容の紹介

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

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

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

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

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

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

スライドおよび発表の模様

以下が発表スライドです。Ustream で発表時の映像も公開 されていますので、観てやろうと云う奇異な方はどうぞ。

反省

参考文献

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

  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 での証明駆動開発の日本語入門文献として挙げておきました。結果的には殆んど何も云えなかったんですが……。

  1. 解説とか採り上げた、ではなくあくまで言及した、です。物によっては名前出しただけですね……。ちゃんと解説したものには★を付けてあります。軽く説明したものは☆です。名前だけ出した、ものは何も付いてません。