(相互)再帰 in full-sessions
忘れた頃に full-sessions の開発をやっている。
これまでセッション型の再帰を扱いづらかったので、もっとイージーに使えるようにした。
unwind という関数で、再帰の開始点を表すことにした*1。 例えば、
{-# LANGUAGE NoMonomorphismRestriction #-} import FullSession -- 単純な再帰プロセス simple c = unwind c >>> send c "abc" >>> simple c
では、チャネルc の使用が再帰的になっていて、これを Haskellの型でどう表現するかという問題がある。
開発中のfull-sessionsでは、simpleの型は
*Main> :t typechekc1 simple
typecheck1 simple
:: (SList ss', SList ss) =>
Session t (ss :> Rec Z (Send [Char] (Var Z))) ss' aとなる*2。 チャネル c のセッション型は Rec Z (Send [Char] (Var Z)) という部分だが、これはちょうど νx. Send [Char] x というセッション型を表現している。 このν記法(Haskellにはない)で、νx.f(x) は x=f(x) の最大不動点を表している。
むろん Haskellの型は structuralではないので Rec Z (Send [Char] (Var Z)) と Send [Char] (Rec Z (Send [String] (Var Z)) という型は別の型として区別され、互換性はない。 -rectypesが欲しいけれど、まあしょうがない。
相互再帰もうまくいった。
-- 相互再帰するセッションを含むプロセス mutual c = unwind c >>> send c "abc" >>> let y = unwind c >>> send c True >>> offer c (mutual c) y in y
はチャネルcの使われ方が相互再帰的になっているが、
*Main> :t typecheck1 mutual
typecheck1 mutual
:: (SList ss', SList ss) =>
Session
t
(ss
:> Rec
Z
(Send [Char] (Rec (S Z) (Send Bool (Offer (Var Z) (Var (S Z)))))))
ss'
a
*Main> のように型が推論される(やったね!)。 このプロセスのチャネル c のセッション型は Rec Z (Send [Char] (Rec (S Z) (Send Bool (Offer (Var Z) (Var (S Z))))))) で、ν記法を使うと νx. Send String (νy. Send Bool (Offer x y)) となる。
相互再帰を扱うために型変数を区別する必要があったので 型変数の比較 で触ったときのテクニックを使った。 このため (元々 GHCでしか動作しないコードだったけれど、さらに) -XIncoherentInstances が必要になっている。
