Coroutine- Type-safe coroutines using lightweight session types.




class IxMonad m whereSource

IxMonad (Indexed Monad) carries type-level state through a computation. For an IxMonad m, m px py a represents a computation with precondition px, postcondition py, and result value a. px and py can be thought of as type-level propositions that hold at the beginning and end of the computation.


return :: a -> m x x aSource

(>>=) :: m x y a -> (a -> m y z b) -> m x z bSource

(>>) :: m x y a -> m y z b -> m x z bSource

fail :: String -> m x y aSource


newtype IxCont s x y a Source

IxCont is a continuation monad that supports changing of the answer type during the computation. The result is a functor s x, where the caller of the computation controls the type held inside the functor.




runIxCont :: forall b. (a -> s y b) -> s x b


mapCont :: (forall a. s x a -> s y a) -> IxCont s x z a -> IxCont s y z aSource

mapCont changes the answer type of an IxCont, given a function that maps any (s x) to a (s y).