On Thu, Dec 18, 2008 at 3:01 AM, Robin Green
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-Instanc... [3] http://comonad.com/reader/2008/zapping-strong-adjunctions/ [4] http://www.ccs.neu.edu/home/tov/pubs/session08.html