[Haskell-cafe] Coroutines

[Ryan Ingram]

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.

In addition, I think coroutines under effectful monads are still
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

[1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/TypeCompose-0.6.3
[2] http://haskell.org/ghc/docs/latest/html/libraries/base/Control-Monad-Instances.html
[3] http://comonad.com/reader/2008/zapping-strong-adjunctions/
[4] http://www.ccs.neu.edu/home/tov/pubs/session08.html