Ryan Ingram ryani.spam at gmail.com
Thu Dec 18 07:22:21 EST 2008

On Thu, Dec 18, 2008 at 3:01 AM, Robin Green <greenrd at greenrd.org> wrote:
> In my opinion, in Haskell, you don't need coroutines because you have
> lazy evaluation.

That's a fair criticism.  Lazy evaluation basically gives you a
coroutine embedded in any data structure.  But sometimes making
implicit things explicit aids understanding! Especially when there can
be communication in both directions; that is, the data structure can
be somewhat dependent on the code doing the evaluation.

potentially useful.  It would not be too hard to extend this library
to allow effectful computations to communicate.  At the very least I
can easily imagine a version of InSession that supports lifting from
IO into coroutines.

> You example below is simply an example of a heterogenous list being
> read. The simplest way to implement a heterogenous list in Haskell is
> to use a tuple. Or you could use the HList package.

Actually, the result of "runSession simple" is isomorphic to a
tuple/heterogeneous list:

> data instance InSession (a :!: r) v = W a (InSession r v)
> newtype instance InSession Eps v = Eps v

runSession simple :: InSession (String :!: Int :!: (Int -> Int) :!: Eps) ()
=> W "hello" $W 1$ W (+1) $Eps () Similarily, useSimple evaluates to a function of three arguments: > newtype instance InSession (a :?: r) v = R (a -> InSession r v) runSession useSimple => R$ \string -> R $\int -> R$ \func -> Eps (string ++ show (int *
4) ++ show (func 10))

There are three pieces to this package:

1) A monad-like structure that gives nice syntax for the construction
of InSession values.

2) A data family that gives a representation of these values as
different functors.  This is similar to using the TypeCompose library
[1] and the (,) a and (->) a Functor instances [2].  That is, in some
way (a :!: r) represents ((,) a) . r.   (.) here represents function
composition at the *type* level.  This allows composition of functors:

(a :!: b :?: c :!: Eps)
== (a,) . (b ->) . (c,) . Id
== \v -> (a, b -> (c,v))

where again, the lambda is at the type level, and (a,) means a section
at the type level similar to (5 <=) at the value level.

(As an aside, my thanks to Simon Peyton-Jones for suggesting this
representation of sessions using type families.)

3) A "duality" type family and connector which shows which functors
can be connected to which other functors.  This is similar to the
"zap" operation in Category-extras [3].

I wrote the library initially to play around with (1); Indexed monads
are an interesting topic and I don't think they are well covered
outside of the dense material by Oleg & friends.  I definitely
understand them much better after writing it!  (2) and (3) are there
to give some structure to the exercise.

The other goal was to give a machine-checkable proof of the semantics
of session types described in Jesse Tov's paper [4].  In the paper,
sessions are represented by effectful computations, which run in
parallel and communicate over *untyped* channels, using unsafeCoerce.
The paper contains a proof that this is indeed safe, but it seemed
worthwhile to encode the proof in the Haskell type system, allowing
the possibility to remove unsafeCoerce.

-- ryan