\section{Session Types in Haskell}
\label{sec:session}
\ignore{
>
> module Control.Concurrent.SimpleSession.SessionTypes (
> Z, S,
> Eps, (:!:), (:?:), (:+:), (:&:), Rec, Var,
> Dual
> ) where
>
> infixr 3 :!:, :?:
> infix 2 :+:, :&:
>
> data Z
> data S n
}
The central idea of session types \citep{r:gay99} is to parameterize a
channel with some type that represents a protocol, which the type system
then enforces. In Haskell, we may encode a protocol using ordinary
datatypes:
> data (:!:) a r
> data (:?:) a r
> data Eps
These datatypes require no constructors because they will have no
run-time representation.
If |a| is any type, and |r| is a protocol, then
we interpret |a :!: r| as the protocol, ``first send an |a|, and
then continue with |r|.'' Similarly, we interpret |a :?: r| as
the protocol, ``receive
an |a|, and then continue with |r|.'' The type |Eps| represents the empty
protocol of a depleted channel that is not yet closed.
For example, the type |Int :!: Bool :?: Eps| represents the protocol,
``send an |Int|, receive a |Bool|, and close the
channel.''\thinspace\footnote{The type constructors |(:!:)| and
|(:?:)| 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}.
> class Dual r s | r -> s, s -> r
The functional dependencies indicate that duality
is bijective, which helps Haskell to infer
protocols and enables a form of subtyping. Sending and receiving are
dual: if |r| is dual to |s|, then |a :!: r| is dual to |a :?: s|. The
empty session is dual to itself.
> instance Dual r s => Dual (a :!: r) (a :?: s)
> instance Dual r s => Dual (a :?: r) (a :!: s)
> instance Dual Eps Eps
\par
Our session types also represent alternation and recursion. If |r|
and |s| are protocols, then |r :+: s| represents an active choice
between following |r| or |s|. The type |r :&: s| represents
an offer to follow either |r| or |s|, as chosen by the other
process.
> data (:+:) r s
> data (:&:) r s
The two alternation operators are dual:
> instance (Dual r1 s1, Dual r2 s2) =>
> Dual (r1 :+: r2) (s1 :&: s2)
> instance (Dual r1 s1, Dual r2 s2) =>
> Dual (r1 :&: r2) (s1 :+: s2)
\par
Recursion turns out to be slightly more difficult. It is tempting to
use a fixed-point combinator, but this would require constructing a
type of kind $\star \to \star$ for any desired loop body, which
is not generally possible. We need
some other way for a recursive type to refer to itself, so we represent
this binding using de~Bruijn indices.
> data Rec r
> data Var v
>
> instance Dual r s => Dual (Rec r) (Rec s)
> instance Dual (Var v) (Var v)
The type |Rec r| adds a binding for |r| inside |r|; that is, it
implicitly defines a variable bound to the whole of |r| that can be used
\emph{within} |r|. We use |Var v| to refer to the variable bound by
the |v|th |Rec|, counting outward, where |v| is a Peano numeral
written with type constructors |Z| and |S|
(\emph{e.g.,} |Z| or |S (S Z)|). For example, the protocol
< Request :!: Rec (Response :?: (Var Z :&: Eps))
says to send a request and then be prepared to receive one or more
responses. By contrast, a process implementing the protocol
< Request :!: Rec ((Response :?: Var Z) :&: Eps)
must send a request and be prepared to accept any number of responses.