> {-# 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 EpsThese 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 -> rThe 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 sThe 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.