SessionTypes.lhs

\section{Session Types in Haskell}
\label{sec:session}

\ignore{

> {-# LANGUAGE TypeOperators,
>              EmptyDataDecls,
>              MultiParamTypeClasses,
>              FunctionalDependencies,
>              UndecidableInstances #-}
> 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.