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.
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
> 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)
=> 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
 and the (,) a and (->) a Functor instances . 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 .
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 . 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.
More information about the Haskell-Cafe