セッションタイプの実装と応用
@keigoi さんのつぶやきを勝手にメモ。
indexed monadが興味深い。
ML使いとしてはphantom typeでどこまでやれるのかも把握しておきたいですね。
-
- いいね！0
Yoichi Hirai
@pirapira
. @keigoi さんがセッション型をHaskellに入れたやり方で、takeMVarとputMVarを呼ぶ回数を型で管理できて、コンパイル時にデッドロックの可能性を(一部?)排除できる気がする。
2012-11-30 11:17:49
Keigo Imai
@keigoi
自分のやり方以前にも Haskell'08 に出た Pucella & Tov の実装(ほか)があります＜セッション型 on Haskell 私の方法は、本田らのπ計算のセッション型システムをなるべく忠実に埋め込んでる点でちょっと違いがあります
2012-11-30 11:42:13
Keigo Imai
@keigoi
あと線形(セッション)型の型文脈をheterogeneous list として indexed monadの事前/事後条件に埋め込むのですが、私のは(1)de Bruijn level indexと型レベル計算を使った工夫があります
2012-11-30 11:45:44
Keigo Imai
@keigoi
ただ型文脈へのアクセスをde Bruijn levelにしたので、do c<-newChan; send c "hello"; みたく書けるのですが、半面、やや複雑な型レベル計算が必要になっています。de Bruijn indexにするとそれはそれで面倒なのですが
2012-11-30 11:48:45
Keigo Imai
@keigoi
そのへん論文にちゃんとかけていません。あとセッション型の分岐はGADTを使ってうまく表せそうだと先のConorMcBrideの論文を読んで思ったのですが、まだ手をだせていない
2012-11-30 11:50:16
Keigo Imai
@keigoi
シングルスレッドならこんな感じになった：HaskellでデッドロックしないMVar https://t.co/EYB9YomX が、並行性がないのであんまり意味ない。あと他のプリミティブは読者へ(ry
2012-11-30 14:48:42