packages feed

Coroutine (empty) → 0.1.0.0

raw patch · 5 files changed

+427/−0 lines, 5 filesdep +basesetup-changed

Dependencies added: base

Files

+ Control/Coroutine.hs view
@@ -0,0 +1,300 @@+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes #-}++{-|+This module allows you to implement coroutines that communicate in a type-safe manner+using lightweight session types.  An abstract group of session \"type-combinators\" are+offered, and implementations are indexed by those types.++Indexed monads are used to thread the session state through the computation.  We+generally use them to implement \"type-level substitution\"; also known as+\"big lambda\".  For example, consider a session++>  session1 :: forall r. Session (Int :?: String :!: r) r Int++This represents a session that reads an Int, then writes a String, and delivers+an Int which can be used in the remainder of the session @r@.  A way to write it+with full type functions (not legal Haskell) would be++>  session1 :: Session (/\r. Int :?: String :!: r) Float++Using the indexed monad bind operator, we can do, for example:++@+  session2 = do+      x <- session1+      put x+@++Now session2 has the type @forall r. (Int :?: String :!: Float :!: r) r ()@++Connecting two sessions is easy; if they are the dual of each other (one reads+where the other writes), just call "connects s1 s2".  If the sessions are not+compatible, you'll get a reasonably readable compile-time error.+-}++module Control.Coroutine (+    module Control.Monad.Indexed,+    WM(..),+    Eps,+    (:?:), (:!:),+    (:&:), (:|:),+    (:?*), (:!*),+    (:++:), (:*),+    Session(..),++    InSession(..),+    -- R, W, O, CL, CAT, StarC, StarS, Stop, Go,+    +    close, get, put, cat, offer, sel1, sel2,+    Loop(..), loopC, loopS, loop,+    runSession,+    +    Dual, Connect(..), connects+) where+import Control.Monad.Indexed+import qualified Prelude as P++-- | WM stands for "wrapped monad"; it wraps any Prelude monad.+-- This doesn't really belong in this module, but exporting it+-- correctly from IxMonad is a real pain.+-- This allows you to use NoImplicitPrelude when writing+-- "main" in the following way:+--+-- @+-- module Main where+-- import Control.Coroutine+-- main = runWM $ do+--           LiftWM $ putStrLn "hello world"+-- @++newtype WM m x y a = LiftWM { runWM :: m a }+instance P.Monad m => IxMonad (WM m) where+    return x = LiftWM (P.return x)+    m >>= f  = LiftWM (runWM m P.>>= runWM . f)+    m >> n   = LiftWM (runWM m P.>> runWM n)+    fail s   = LiftWM (P.fail s)++-- ; to work around Haddock parse error+--+--   Session            Meaning+data Eps           ;-- ^ @Eps@ is the empty session.+data (:?:) a r     ;-- ^ @a :?: r@ reads @a@ followed by the session @r@+data (:!:) a r     ;-- ^ @a :!: r@ writes @a@ followed by the sesison @r@+data (:&:) s1 s2   ;-- ^ @a :&: b@ offers both the sessions @a@ and @b@ to the other end+data (:|:) s1 s2   ;-- ^ @a :|: b@ allows the choice between sessions @a@ and @b@ at runtime+data (:?*) s r     ;-- ^ @a :?* b@ is the session @a@ zero or more times followed by @b@, offering the loop.+data (:!*) s r     ;-- ^ @a :!* b@ is the session @a@ zero or more times followed by @b@, choosing whether or not to loop.+data (:*) s r      ;-- ^ @a :* b@ is the session @a@ zero or more times followed by @b@.  Either side may terminate the loop.++-- | @a :++: b@ is session @a@ followed by session @b@.+-- This is mostly used for constructing looping constructs;+-- you generally won't need to use it yourself.+data (:++:) s1 s2  --  "Concat"++-- | InSession s v is a functor type representing a session that results in the value v+-- being computed by the session.  s should be indexed by one of the session types above,+-- although you can extended the session type system by adding additional instances+-- here and to Dual and Connect below.+data family InSession s v+newtype instance InSession Eps v        = Eps v+newtype instance InSession (a :?: r) v  = R (a -> InSession r v)+data    instance InSession (a :!: r) v  = W a (InSession r v)+data    instance InSession (a :&: b) v  = O (InSession a v) (InSession b v)+data    instance InSession (a :|: b) v  = CL (InSession a v) | CR (InSession b v)+data    instance InSession (a :++: b) v = forall z. CAT (InSession a z) (z -> InSession b v)+newtype instance InSession (a :!* r) v  = StarC (InSession (r :|: (a :++: (a :!* r))) v)+newtype instance InSession (a :?* r) v  = StarS (InSession (r :&: (a :++: (a :?* r))) v)+data    instance InSession (a :* r) v   = Stop (InSession r v)+                                        | Go   (InSession (r :&: (a :++: (a :* r))) v)++-- | By indexing using a data family, we get an untagged representation of the+-- session; resolving how to link sessions together with "connect" can happen+-- at compile-time.  A similar encoding is possible using GADTs, but it requires+-- runtime branching based on the GADT tag.+--+-- @IxCont s x y a@ == @forall b. (a -> s y b) -> s x b@; that is, if you give us+-- a continuation function that takes an "a" and outputs the rest of the session,+-- we can give you a representation of the full session.  When a session is+-- complete, @y@ is @Eps@, the empty session, so getting the full session out+-- is just @runIxCont (getSession session) Eps@ which gives you the result of type+-- @InSession session_type a@+newtype Session x y a = Session { getSession :: IxCont InSession x y a }+   deriving (IxMonad)++mkSession = Session . IxCont+unSession = runIxCont . getSession++mapSession :: (forall a. InSession s1 a -> InSession s2 a) -> Session s1 r b -> Session s2 r b+mapSession f m = Session $ mapCont f $ getSession m++-- | You never /need/ to explicitly call close; doing so just seals the+-- \"rest-of-computation\" parameter of the session.+close :: Session Eps Eps ()+close = return ()++-- | get reads an element from the connected coroutine+get :: Session (a :?: r) r a+get = mkSession $ \k -> R $ \a -> k a++-- | put x sends the value x to the connected coroutine+put :: a -> Session (a :!: r) r ()+put a = mkSession $ \k -> W a $ k ()++-- | cat m takes a completed session and connects it at+-- the beginning of a sequence inside another session.+cat :: Session a Eps v -> Session (a :++: r) r v+cat s = mkSession $ \k -> CAT (runSession s) k++-- | offer s1 s2 gives the other side the choice of whether+-- to continue with session s1 or s2.+offer :: Session a r v -> Session b r v -> Session (a :&: b) r v+offer sa sb = mkSession $ \k -> O (unSession sa k) (unSession sb k)++-- | sel1 chooses the first branch of an offer+sel1 :: Session (a :|: b) a ()+sel1 = mkSession $ \k -> CL (k ())++-- | sel2 chooses the second branch of an offer+sel2 :: Session (a :|: b) b ()+sel2 = mkSession $ \k -> CR (k ())++-- | Loop is just nicely-named Either; it is used for+-- choosing whether or not to loop in these simplified looping+-- primitives.+data Loop a b = Loop a | Done b++-- | loopC is the client side of a "while" loop; it takes the current+-- loop state, and a computation that figures out the next loop state,+-- and loops until the computation returns "Done".+loopC :: Loop a b                         -- ^ Initial loop state+      -> (a -> Session x Eps (Loop a b))  -- ^ Session for the loop+      -> Session (x :!* r) r b            -- ^ Result of the loop++loopC (Done b) _ = mapSession StarC $ do+    sel1+    return b+loopC (Loop a) f = mapSession StarC $ do+    sel2+    a' <- cat (f a)+    loopC a' f++-- | loopS is the server side of a "while" loop; it must always offer+-- the client the option to terminate the loop at each iteration, or+-- to continue the loop.+loopS :: a                      -- ^ Initial loop state+      -> (a -> Session x Eps a) -- ^ Session for the loop+      -> Session (x :?* r) r a  -- ^ Result of the loop++loopS a f = mapSession StarS $ offer (return a) $ do+     a' <- cat (f a)+     loopS a' f++-- | loop is a slightly more complicated looping primitive where either+-- side of the loop may choose to terminate the loop at each iteration.+-- It is useful for a server that has a fixed amount of data to give out,+-- when the client can also choose to escape early.++loop :: Loop a b                        -- ^ Initial loop state+     -> (a -> Session x Eps (Loop a b)) -- ^ Session for the loop+     -> Session (x :* r) r (Either a b) -- ^ Result of the loop++loop (Done b) _ = mapSession Stop $ return (Right b)+loop (Loop a) f = mapSession Go $ offer (return (Left a)) $ do+    a' <- cat (f a)+    loop a' f++-- | runSession converts a session computation into a "connectable"+-- session.+runSession :: Session c Eps a -> InSession c a+runSession m = unSession m Eps++++-- Connection logic follows; it requires the "Dual" type-logic+-- that connects "reads" to "writes" in the type system.++type family Dual a+type instance Dual Eps        = Eps+type instance Dual (a :?: r)  = a :!: Dual r+type instance Dual (a :!: r)  = a :?: Dual r+type instance Dual (r :&: s)  = Dual r :|: Dual s+type instance Dual (r :|: s)  = Dual r :&: Dual s+type instance Dual (r :++: s) = Dual r :++: Dual s+type instance Dual (r :?* s)  = Dual r :!* Dual s+type instance Dual (r :!* s)  = Dual r :?* Dual s+type instance Dual (r :* s)   = Dual r :*  Dual s++-- would like to put+-- class (Dual (Dual s) ~ s) => Connect s where ...+-- but that doesn't work with GHC 6.10.+class Connect s where+    connect :: (s ~ Dual c, c ~ Dual s) => InSession s a -> InSession c b -> (a, b)++instance Connect Eps where+    connect (Eps a) (Eps b) = (a,b)+instance Connect s => Connect (a :?: s) where+    connect (R k) (W a c) = connect (k a) c+instance Connect s => Connect (a :!: s) where+    connect (W a s) (R k) = connect s (k a)+instance (Connect s1, Connect s2) => Connect (s1 :&: s2) where+    connect (O s _) (CL c) = connect s c+    connect (O _ s) (CR c) = connect s c+instance (Connect s1, Connect s2) => Connect (s1 :|: s2) where+    connect (CL s) (O c _) = connect s c+    connect (CR s) (O _ c) = connect s c+instance (Connect s1, Connect s2) => Connect (s1 :++: s2) where+    connect (CAT s ks) (CAT c kc) =+        case connect s c of+            (vs, vc) -> connect (ks vs) (kc vc)+instance (Connect s1, Connect s2) => Connect (s1 :?* s2) where+    connect (StarS s) (StarC c) = connect s c+instance (Connect s1, Connect s2) => Connect (s1 :!* s2) where+    connect (StarC s) (StarS c) = connect s c+instance (Connect s1, Connect s2) => Connect (s1 :* s2) where+    connect (Stop s)     (Stop c)     = connect s c+    connect (Stop s)     (Go (O c _)) = connect s c+    connect (Go (O s _)) (Stop c)     = connect s c+    connect (Go (O _ s)) (Go (O _ c)) = connect s c++-- | connect two completed sessions to each other+connects :: (Connect s, Dual s ~ c, Dual c ~ s) => Session s Eps a -> Session c Eps b -> (a,b)+connects s c = connect (runSession s) (runSession c)++-- some tests++add_server n = runSession $ do+    loopS n $ \n -> do+        x <- get+        let n' = n + x+        put n'+        return n'+    close++mul_server n = runSession $ do+    loopS n $ \n -> do+        x <- get+        let n' = n * x+        put n'+        return n'+    close++num_client k = runSession $ do+    x <- loopC (Loop (2,[])) $ \(n,l) -> do+        put n+        n' <- get+        let l' = n' : l+        if n' > k then return (Done l')+                  else return (Loop (n', l'))+    close+    return x++list_server l = loop (listdata l) listserv >> close+  where+    listdata []     = Done ()+    listdata (x:xs) = Loop (x,xs)+    +    listserv (x,xs) = put x >> return (listdata xs)
+ Control/Monad/Indexed.hs view
@@ -0,0 +1,73 @@+{-# OPTIONS_HADDOCK ignore-exports #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE RankNTypes #-}+module Control.Monad.Indexed (+    module Prelude,+    IxMonad(..),+    IxCont(..),+    mapCont+) where+import Prelude hiding (Monad(..))++-- | 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.+class IxMonad m where+    return :: a -> m x x a+    (>>=)  :: m x y a -> (a -> m y z b) -> m x z b+    (>>)   :: m x y a -> m y z b -> m x z b+    fail   :: String -> m x y a++    m >> n = m >>= const n+    fail = error++-- | 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.+newtype IxCont s x y a = IxCont { runIxCont ::  forall b. (a -> s y b) -> s x b }++-- | mapCont changes the answer type of an IxCont, given a function+-- that maps any (s x) to a (s y).+mapCont :: (forall a. s x a -> s y a) -> IxCont s x z a -> IxCont s y z a+mapCont f (IxCont k) = IxCont (f . k)++instance IxMonad (IxCont s) where+    return x = IxCont $ \k -> k x+    m >>= g  = IxCont $ \k -> runIxCont m $ \a -> runIxCont (g a) k++{-++-------------------------------------------+- Derivation of bind operator in System F -+- /\r. = type lambda      @r = type apply -+- (haskell: forall r)  (haskell: omitted) -+-------------------------------------------++m >>= g  {pattern}++{from type of >>=}+m :: IxCont s x y a+g :: a -> IxCont s y z b++runIxCont m :: /\c. (a -> s y c) -> s x c {newtype}++IxCont ?1 :: IxCont s x z b++    ?1 :: /\r. (b -> s z r) -> s x r+    ?1 = /\r. \k -> ...+        k :: b -> s z r+        runIxCont m @r ?2 :: s x r+    ?1 = /\r. \k -> f @r ?2++    ?2 :: a -> s y r+    ?2 = \a -> ...+        a :: a+        g a :: IxCont s y z b+        runIxCont (g a) :: /\c. (b -> s z c) -> s y c+        runIxCont (g a) @r k :: s y r+    ?2 = \a -> runIxCont (g a) @r k++-}
+ Coroutine.cabal view
@@ -0,0 +1,29 @@+name:            Coroutine+version:         0.1.0.0+copyright:       (c) 2008 Ryan Ingram+license:         BSD3+license-file:    LICENSE+author:          Ryan Ingram <ryani.spam@gmail.com>+maintainer:      Ryan Ingram <ryani.spam@gmail.com>+category:        Control+synopsis:        Type-safe coroutines using lightweight session types.+description:     This package provides a pure interface for composing+                 independent functions that have a well-defined+                 communication protocol.+                 It is loosely based on Jesse Tov's Haskell Symposium 2008+                 paper "Haskell Session Types with (almost) no class"+                 (http://www.ccs.neu.edu/home/tov/pubs/session08.html)+stability:       experimental+build-type:      Simple+cabal-version:   >= 1.2.1++library+  exposed-modules: Control.Coroutine,+                   Control.Monad.Indexed+  extensions:      NoImplicitPrelude, +                   EmptyDataDecls,+                   TypeFamilies,+                   RankNTypes,+                   TypeOperators,+                   ExistentialQuantification+  build-depends:   base >= 3.0
+ LICENSE view
@@ -0,0 +1,23 @@+Copyright (c) 2008, Ryan Ingram+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice,+   this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain