Control.Concurrent.SimpleSession.SessionTypes

Documentation

data Z

Instances

Pop (Cap (r, e) (Var Z)) (Cap (r, e) r)

data S n

Instances

Pop (Cap e (Var v)) (Cap e' r') => Pop (Cap (r, e) (Var (S v))) (Cap e' r')

data Eps

Instances

Dual Eps Eps

data a :!: r

Instances

Dual r s => Dual (:?: a r) (:!: a s)

Dual r s => Dual (:!: a r) (:?: a s)

data a :?: r

Instances

Dual r s => Dual (:?: a r) (:!: a s)

Dual r s => Dual (:!: a r) (:?: a s)

data r :+: s

Instances

(Dual r1 s1, Dual r2 s2) => Dual (:&: r1 r2) (:+: s1 s2)

(Dual r1 s1, Dual r2 s2) => Dual (:+: r1 r2) (:&: s1 s2)

data r :&: s

Instances

(Dual r1 s1, Dual r2 s2) => Dual (:&: r1 r2) (:+: s1 s2)

(Dual r1 s1, Dual r2 s2) => Dual (:+: r1 r2) (:&: s1 s2)

data Rec r

Instances

Dual r s => Dual (Rec r) (Rec s)

data Var v

Instances

Dual (Var v) (Var v)

Pop (Cap e (Var v)) (Cap e' r') => Pop (Cap (r, e) (Var (S v))) (Cap e' r')

Pop (Cap (r, e) (Var Z)) (Cap (r, e) r)

class Dual r s | r -> s, s -> r

(:?:)| are declared right associative and with higher precedence than |(:+:)| and |(:&:)|.}

If the process on one end of a channel speaks a particular protocol, its correspondant at the other end of the channel must be prepared to understand it. For example, if one process speaks |Int :!: Bool :?: Eps|, the other process must implement the dual protocol |Int :?: Bool :!: Eps|. We encode the duality relation using a type class with multiple parameters and functional dependencies citep{Jones1997Type,Jones2000Type}.

Instances

Dual Eps Eps

Dual (Var v) (Var v)

Dual r s => Dual (Rec r) (Rec s)

(Dual r1 s1, Dual r2 s2) => Dual (:&: r1 r2) (:+: s1 s2)

(Dual r1 s1, Dual r2 s2) => Dual (:+: r1 r2) (:&: s1 s2)

Dual r s => Dual (:?: a r) (:!: a s)

Dual r s => Dual (:!: a r) (:?: a s)