既存の セッション型の実装 on Haskell

Haskell full-sessions 研究

セッション型のような型は，関数型言語の型システムでは作れないのが普通だ．しかしながらセッション型の機能の一部を関数型言語で実現しようとする試みはいくつか存在する． つい最近では， Kiselyov, Peyton Jones, Shanの Fun with type functions のように，チャネルを1つに，スレッドを2つ限定した形での実装がある． 元々は Neubauer, Thiemann らの An implementation of session typesに端を発する． (私も似たようなものを書いて国内の研究会で発表したことがある．)
さらに Pucella, Tov の Haskell '08 の Haskell Session Types with (Almost) No Class，Sackmanらの Session Types in Haskell: Updating Message Passing for the 21st Century (論文) は，アノテーションを加えることで Haskell (Pucellaらの実装は C#, Java, OCaml, Scala, SMLでも!) 上にセッション型のフル実装を実現している． これらは Hackageでも提供されており， cabal install 一発でインストールできる．

私の実装

私の実装は，上の例のように，アノテーションをほぼ完全に取り除いた形でのセッション型を提供する．

Sackmanの実装は，セッション型に対応する項を記述し，さらにプログラム本体を記述しなければならない．一方，Pucellaらの実装では， 複数のチャネルを扱う際に swap と dig というアノテーションで 「現在使っているチャネル」を管理しなければならない．(その代わり，Pucellaらの実装はtype-classなしで実装できている)

私の実装では，型レベル計算を駆使することで，このようなアノテーションをほぼ無くすことに成功している．