simple-sessions-0.1: A simple implementation of session types




data Session s s' a Source

Session| is implemented as the composition of the IO monad with a reader monad carrying a untyped channel.

data Cap e r Source


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) 

io :: IO a -> Session s s aSource

send :: a -> Session (Cap e (a :!: r)) (Cap e r) ()Source

recv :: Session (Cap e (a :?: r)) (Cap e r) aSource

a :!: r| to |r|. In its implementation, |unsafeWriteUChan| indiscriminately transmits values of any type over an untyped channel. Thus, if we fail to ensure that the receiving process expects a value of type |a|, things can go very wrong. In Sectionref{sec:theory}, we argue that this cannot happen.

Predictably, |recv| requires the capability to receive an |a|, which it then produces:

sel1 :: Session (Cap e (r :+: s)) (Cap e r) ()Source

Session|, this does not jeopardize safety in the sense that any messages received will still have the expected representation. Some formulations of session types guarantee that a session, once initiated, will run to completion, but this seems unrealistic for real-world programs. Handling exceptions from within a session remains an open problem.


The session actions |sel1|, |sel2|, and |offer| implement alternation. Action |sel1| selects the left side of an ``internal choice'', thereby replacing a session |r :+: s| with the session |r|; |sel2| selects the right side. On the other side of the channel, |offer| combines a |Session| computation for |r| with a computation for |s| into a computation that can handle |r :&: s|. Dynamically, |sel1| sends |True| over the channel, whereas |sel2| sends |False|, and |offer| dispatches on the boolean value received.

sel2 :: Session (Cap e (r :+: s)) (Cap e s) ()Source

offer :: Session (Cap e r) u a -> Session (Cap e s) u a -> Session (Cap e (r :&: s)) u aSource

enter :: Session (Cap e (Rec r)) (Cap (r, e) r) ()Source

zero :: Session (Cap (r, e) (Var Z)) (Cap (r, e) r) ()Source

Rec|, representing an environment that closes over |r|. Upon encountering a variable occurence |Var |$n$, where $n$ is a Peano numeral, we restore the $n$th session type from the stack and return the stack to its former state, using $n$ expressed with |zero| and |suc|:

suc :: Session (Cap (r, e) (Var (S v))) (Cap e (Var v)) ()Source

class Pop s s' | s -> s' whereSource


pop :: Session s s' ()Source


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) 

request :: Dual r r' => Rendezvous r -> Session (Cap () r') () a -> IO aSource

request| receives a new, untyped channel from |accept| over the |Rendezvous| channel and then runs the computation using the channel.