diff --git a/Control/CCCxe.hs b/Control/CCCxe.hs new file mode 100644 --- /dev/null +++ b/Control/CCCxe.hs @@ -0,0 +1,251 @@ +{-# LANGUAGE PatternGuards, KindSignatures #-} +{-# LANGUAGE ExistentialQuantification, RankNTypes, ImpredicativeTypes #-} + +-- This file is the CPS version of CCExc.hs, implementing the identical +-- interface +-- +-- +-- +-- Monad transformer for multi-prompt delimited control +-- It implements the superset of the interface described in +-- +-- > A Monadic Framework for Delimited Continuations +-- > R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry +-- > JFP, v17, N6, pp. 687--730, 2007. +-- > http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR615 +-- +-- The first main difference is the use of generalized prompts, which +-- do not have to be created with new_prompt and therefore can be defined +-- at top level. That removes one of the main practical drawbacks of +-- Dybvig et al implementations: the necessity to carry around the prompts +-- throughout all the code. +-- +-- The delimited continuation monad is parameterized by the flavor +-- of generalized prompts. The end of this code defines several flavors; +-- the library users may define their own. User-defined flavors are +-- especially useful when user's code uses a small closed set of answer-types. +-- Flavors PP and PD below are more general, assuming the set of possible +-- answer-types is open and Typeable. If the user wishes to create several +-- distinct prompts with the same answer-types, the user should use +-- the flavor of prompts accepting an integral prompt identifier, such as PD. +-- Prompts of the flavor PD correspond to the prompts in Dybvig, Peyton Jones, +-- Sabry framework. If the user wishes to generate unique prompts, the user +-- should arrange himself for the generation of unique integers +-- (using a state monad, for example). On the other hand, the user +-- can differentiate answer-types using `newtype.' The latter can +-- only produce the set of distinct prompts that is fixed at run-time. +-- Sometimes that is sufficient. There is not need to create a gensym +-- monad then. +-- +-- See CCExc.hs for further comments about the implementation + +module Control.CCCxe ( + CC, -- Types + SubCont, + CCT, + Prompt, + + -- Basic delimited control operations + pushPrompt, + takeSubCont, + pushSubCont, + runCC, + + -- Useful derived operations + abortP, + shiftP, + shift0P, + controlP, + + -- Pre-defined prompt flavors + PS, ps, + P2, p2L, p2R, + PP, pp, + PM, pm, + PD, newPrompt, + as_prompt_type + ) where + +import Control.Monad.Trans +import Data.Typeable -- for prompts of the flavor PP, PD + +-- | Delimited-continuation monad transformer +-- It is parameterized by the prompt flavor p +-- The first argument is the regular (success) continuation, +-- the second argument is the bubble, or a resumable exception +newtype CC p m a = + CC{unCC:: forall w. (a -> m w) -> + (forall x. SubCont p m x a -> p m x -> m w) -> + m w} + +-- | The captured sub-continuation +type SubCont p m a b = CC p m a -> CC p m b + +-- | The type of control operator's body +type CCT p m a w = SubCont p m a w -> CC p m w + +-- | Generalized prompts for the answer-type w: an injection-projection pair +type Prompt p m w = + (forall x. CCT p m x w -> p m x, + forall x. p m x -> Maybe (CCT p m x w)) + + +-- -------------------------------------------------------------------- +-- | CC monad: general monadic operations +-- +instance Monad m => Monad (CC p m) where + return x = CC $ \ki kd -> ki x + + m >>= f = CC $ \ki kd -> unCC m + (\a -> unCC (f a) ki kd) + (\ctx -> kd (\x -> ctx x >>= f)) + +instance MonadTrans (CC p) where + lift m = CC $ \ki kd -> m >>= ki + +instance MonadIO m => MonadIO (CC p m) where + liftIO = lift . liftIO + +-- -------------------------------------------------------------------- +-- | Basic Operations of the delimited control interface +-- +pushPrompt :: Monad m => + Prompt p m w -> CC p m w -> CC p m w +pushPrompt p@(_,proj) body = CC $ \ki kd -> + let kd' ctx body | Just b <- proj body = unCC (b ctx) ki kd + kd' ctx body = kd (\x -> pushPrompt p (ctx x)) body + in unCC body ki kd' + + +-- | Create the initial bubble +takeSubCont :: Monad m => + Prompt p m w -> CCT p m x w -> CC p m x +takeSubCont p@(inj,_) body = CC $ \ki kd -> kd id (inj body) + +-- | Apply the captured continuation +pushSubCont :: Monad m => SubCont p m a b -> CC p m a -> CC p m b +pushSubCont = ($) + +runCC :: Monad m => CC (p :: (* -> *) -> * -> *) m a -> m a +runCC m = unCC m return err + where + err = error "Escaping bubble: you have forgotten pushPrompt" + + +-- -------------------------------------------------------------------- +-- | Useful derived operations +-- +abortP :: Monad m => + Prompt p m w -> CC p m w -> CC p m any +abortP p e = takeSubCont p (\_ -> e) + +shiftP :: Monad m => + Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a +shiftP p f = takeSubCont p $ \sk -> + pushPrompt p (f (\c -> + pushPrompt p (pushSubCont sk (return c)))) + +shift0P :: Monad m => + Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a +shift0P p f = takeSubCont p $ \sk -> + f (\c -> + pushPrompt p (pushSubCont sk (return c))) + +controlP :: Monad m => + Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a +controlP p f = takeSubCont p $ \sk -> + pushPrompt p (f (\c -> + pushSubCont sk (return c))) + +-- -------------------------------------------------------------------- +-- Prompt flavors + +-- | The extreme case: prompts for the single answer-type w. +-- The monad (CC PS) then is the monad for regular (single-prompt) +-- delimited continuations +newtype PS w m x = PS (CCT (PS w) m x w) + +-- | There is only one generalized prompt of the flavor PS for a +-- given answer-type w. It is defined below +ps :: Prompt (PS w) m w +ps = (inj, prj) + where + inj = PS + prj (PS x) = Just x + +-- | Prompts for the closed set of answer-types +-- The following prompt flavor P2, for two answer-types w1 and w2, +-- is given as an example. Typically, a programmer would define their +-- own variant data type with variants for the answer-types that occur +-- in their program. +-- +newtype P2 w1 w2 m x = + P2 (Either (CCT (P2 w1 w2) m x w1) (CCT (P2 w1 w2) m x w2)) + + +-- | There are two generalized prompts of the flavor P2" +p2L :: Prompt (P2 w1 w2) m w1 +p2L = (inj, prj) + where + inj = P2 . Left + prj (P2 (Left x)) = Just x + prj _ = Nothing + +p2R :: Prompt (P2 w1 w2) m w2 +p2R = (inj, prj) + where + inj = P2 . Right + prj (P2 (Right x)) = Just x + prj _ = Nothing + + +-- | Prompts for the open set of answer-types +-- +data PP m x = forall w. Typeable w => PP (CCT PP m x w) + +-- | We need to wrap the type alias CCT into a newtype. Otherwise, gcast +-- doesn't work. We can't treat (CCT p m a w) as a an application of +-- the `type constructor' (CCT p m a) to the type w: type aliases can't +-- be partially applied. But we can treat the type (NCCT p m a w) that way. +newtype NCCT p m a w = NCCT{unNCCT :: CCT p m a w} + +pp :: Typeable w => Prompt PP m w +pp = (inj, prj) + where + inj = PP + prj (PP c) = maybe Nothing (Just . unNCCT) (gcast (NCCT c)) + +-- | The same as PP but with the phantom parameter c +-- The parameter is useful to statically enforce various constrains +-- (statically pass some information between shift and reset) +-- The prompt PP is too `dynamic': all errors are detected dynamically +-- See Generator2.hs for an example +data PM c m x = forall w. Typeable w => PM (CCT (PM c) m x w) + +pm :: Typeable w => Prompt (PM c) m w +pm = (inj, prj) + where + inj = PM + prj (PM c) = maybe Nothing (Just . unNCCT) (gcast (NCCT c)) + +-- | Open set of answer types, with an additional distinction (given by +-- integer identifiers) +-- This prompt flavor corresponds to the prompts in the Dybvig, Peyton-Jones, +-- Sabry framework (modulo the Typeable constraint). +-- +data PD m x = forall w. Typeable w => PD Int (CCT PD m x w) + +newPrompt :: Typeable w => Int -> Prompt PD m w +newPrompt mark = (inj, prj) + where + inj = PD mark + prj (PD mark' c) | mark' == mark, + Just (NCCT x) <- gcast (NCCT c) = Just x + prj _ = Nothing + +-- | It is often helpful, for clarity of error messages, to specify the +-- answer-type associated with the prompt explicitly (rather than relying +-- on the type inference to figure that out). The following function +-- is useful for that purpose. +as_prompt_type :: Prompt p m w -> w -> Prompt p m w +as_prompt_type = const diff --git a/Control/CCExc.hs b/Control/CCExc.hs new file mode 100644 --- /dev/null +++ b/Control/CCExc.hs @@ -0,0 +1,258 @@ +{-# LANGUAGE PatternGuards, KindSignatures #-} +{-# LANGUAGE ExistentialQuantification, Rank2Types, ImpredicativeTypes #-} + +-- | Monad transformer for multi-prompt delimited control +-- It implements the superset of the interface described in +-- +-- +-- +-- > A Monadic Framework for Delimited Continuations +-- > R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry +-- > JFP, v17, N6, pp. 687--730, 2007. +-- > http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR615 +-- +-- The first main difference is the use of generalized prompts, which +-- do not have to be created with new_prompt and therefore can be defined +-- at top level. That removes one of the main practical drawbacks of +-- Dybvig et al implementations: the necessity to carry around the prompts +-- throughout all the code. +-- +-- The delimited continuation monad is parameterized by the flavor +-- of generalized prompts. The end of this code defines several flavors; +-- the library users may define their own. User-defined flavors are +-- especially useful when user's code uses a small closed set of answer-types. +-- Flavors PP and PD below are more general, assuming the set of possible +-- answer-types is open and Typeable. If the user wishes to create several +-- distinct prompts with the same answer-types, the user should use +-- the flavor of prompts accepting an integral prompt identifier, such as PD. +-- Prompts of the flavor PD correspond to the prompts in Dybvig, Peyton Jones, +-- Sabry framework. If the user wishes to generate unique prompts, the user +-- should arrange himself for the generation of unique integers +-- (using a state monad, for example). On the other hand, the user +-- can differentiate answer-types using `newtype.' The latter can +-- only produce the set of distinct prompts that is fixed at run-time. +-- Sometimes that is sufficient. There is not need to create a gensym +-- monad then. +-- +-- The second feature of our implementation is the use of the +-- bubble-up semantics: +-- See page 57 of +-- This present code implements, for the first time, the delimited +-- continuation monad CC *without* the use of the continuation monad. +-- This code implements CC in direct-style, so to speak. +-- Instead of continuations, we rely on exceptions. Our code has a lot +-- in common with the Error monad. In fact, our code implements +-- an Error monad for resumable exceptions. + +module Control.CCExc ( + CC, -- Types + SubCont, + CCT, + Prompt, + + -- Basic delimited control operations + pushPrompt, + takeSubCont, + pushSubCont, + runCC, + + -- Useful derived operations + abortP, + shiftP, + shift0P, + controlP, + + -- Pre-defined prompt flavors + PS, ps, + P2, p2L, p2R, + PP, pp, + PM, pm, + PD, newPrompt, + as_prompt_type + ) where + +import Control.Monad.Trans +import Data.Typeable -- for prompts of the flavor PP, PD + +-- | Delimited-continuation monad transformer +-- It is parameterized by the prompt flavor p +newtype CC p m a = CC{unCC:: m (CCV p m a)} + +-- | The captured sub-continuation +type SubCont p m a b = CC p m a -> CC p m b + +-- | Produced result: a value or a resumable exception +data CCV p m a = Iru a + | forall x. Deru (SubCont p m x a) (p m x) -- The bubble + +-- | The type of control operator's body +type CCT p m a w = SubCont p m a w -> CC p m w + +-- | Generalized prompts for the answer-type w: an injection-projection pair +type Prompt p m w = + (forall x. CCT p m x w -> p m x, + forall x. p m x -> Maybe (CCT p m x w)) + + +-- +-- |CC monad: general monadic operations +-- +instance Monad m => Monad (CC p m) where + return = CC . return . Iru + + m >>= f = CC $ unCC m >>= check + where check (Iru a) = unCC $ f a + check (Deru ctx body) = return $ Deru (\x -> ctx x >>= f) body + + +instance MonadTrans (CC p) where + lift m = CC (m >>= return . Iru) + +instance MonadIO m => MonadIO (CC p m) where + liftIO = lift . liftIO + +-- +-- | Basic Operations of the delimited control interface +-- +pushPrompt :: Monad m => + Prompt p m w -> CC p m w -> CC p m w +pushPrompt p@(_,proj) body = CC $ unCC body >>= check + where + check e@Iru{} = return e + check (Deru ctx body) | Just b <- proj body = unCC $ b ctx + check (Deru ctx body) = return $ Deru (\x -> pushPrompt p (ctx x)) body + + +-- | Create the initial bubble +takeSubCont :: Monad m => + Prompt p m w -> CCT p m x w -> CC p m x +takeSubCont p@(inj,_) body = CC . return $ Deru id (inj body) + +-- Apply the captured continuation +pushSubCont :: Monad m => SubCont p m a b -> CC p m a -> CC p m b +pushSubCont = ($) + +runCC :: Monad m => CC (p :: (* -> *) -> * -> *) m a -> m a +runCC m = unCC m >>= check + where + check (Iru x) = return x + check _ = error "Escaping bubble: you have forgotten pushPrompt" + + +-- -------------------------------------------------------------------- +-- | Useful derived operations +-- +abortP :: Monad m => + Prompt p m w -> CC p m w -> CC p m any +abortP p e = takeSubCont p (\_ -> e) + +shiftP :: Monad m => + Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a +shiftP p f = takeSubCont p $ \sk -> + pushPrompt p (f (\c -> + pushPrompt p (pushSubCont sk (return c)))) + +shift0P :: Monad m => + Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a +shift0P p f = takeSubCont p $ \sk -> + f (\c -> + pushPrompt p (pushSubCont sk (return c))) + +controlP :: Monad m => + Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a +controlP p f = takeSubCont p $ \sk -> + pushPrompt p (f (\c -> + pushSubCont sk (return c))) + +-- -------------------------------------------------------------------- +-- Prompt flavors + +-- | The extreme case: prompts for the single answer-type w. +-- The monad (CC PS) then is the monad for regular (single-prompt) +-- delimited continuations +newtype PS w m x = PS (CCT (PS w) m x w) + +-- | There is only one generalized prompt of the flavor PS for a +-- given answer-type w. It is defined below +ps :: Prompt (PS w) m w +ps = (inj, prj) + where + inj = PS + prj (PS x) = Just x + +-- | Prompts for the closed set of answer-types +-- The following prompt flavor P2, for two answer-types w1 and w2, +-- is given as an example. Typically, a programmer would define their +-- own variant data type with variants for the answer-types that occur +-- in their program. +-- +newtype P2 w1 w2 m x = + P2 (Either (CCT (P2 w1 w2) m x w1) (CCT (P2 w1 w2) m x w2)) + + +-- | There are two generalized prompts of the flavor P2: +p2L :: Prompt (P2 w1 w2) m w1 +p2L = (inj, prj) + where + inj = P2 . Left + prj (P2 (Left x)) = Just x + prj _ = Nothing + +p2R :: Prompt (P2 w1 w2) m w2 +p2R = (inj, prj) + where + inj = P2 . Right + prj (P2 (Right x)) = Just x + prj _ = Nothing + + +-- | Prompts for the open set of answer-types +-- +data PP m x = forall w. Typeable w => PP (CCT PP m x w) + +-- | We need to wrap the type alias CCT into a newtype. Otherwise, gcast +-- doesn't work. We can't treat (CCT p m a w) as a an application of +-- the `type constructor' (CCT p m a) to the type w: type aliases can't +-- be partially applied. But we can treat the type (NCCT p m a w) that way. +newtype NCCT p m a w = NCCT{unNCCT :: CCT p m a w} + +pp :: Typeable w => Prompt PP m w +pp = (inj, prj) + where + inj = PP + prj (PP c) = maybe Nothing (Just . unNCCT) (gcast (NCCT c)) + +-- | The same as PP but with the phantom parameter c +-- The parameter is useful to statically enforce various constrains +-- (statically pass some information between shift and reset) +-- The prompt PP is too `dynamic': all errors are detected dynamically +-- See Generator2.hs for an example +data PM c m x = forall w. Typeable w => PM (CCT (PM c) m x w) + +pm :: Typeable w => Prompt (PM c) m w +pm = (inj, prj) + where + inj = PM + prj (PM c) = maybe Nothing (Just . unNCCT) (gcast (NCCT c)) + +-- | Open set of answer types, with an additional distinction (given by +-- integer identifiers) +-- This prompt flavor corresponds to the prompts in the Dybvig, Peyton-Jones, +-- Sabry framework (modulo the Typeable constraint). +-- +data PD m x = forall w. Typeable w => PD Int (CCT PD m x w) + +newPrompt :: Typeable w => Int -> Prompt PD m w +newPrompt mark = (inj, prj) + where + inj = PD mark + prj (PD mark' c) | mark' == mark, + Just (NCCT x) <- gcast (NCCT c) = Just x + prj _ = Nothing + +-- | It is often helpful, for clarity of error messages, to specify the +-- answer-type associated with the prompt explicitly (rather than relying +-- on the type inference to figure that out). The following function +-- is useful for that purpose. +as_prompt_type :: Prompt p m w -> w -> Prompt p m w +as_prompt_type = const diff --git a/Control/CCRef.hs b/Control/CCRef.hs new file mode 100644 --- /dev/null +++ b/Control/CCRef.hs @@ -0,0 +1,628 @@ +-- | Monad transformer for multi-prompt delimited control +-- +-- This library implements the superset of the interface described in +-- +-- > A Monadic Framework for Delimited Continuations +-- > R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry +-- > JFP, v17, N6, pp. 687--730, 2007. +-- > http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR615 +-- +-- This code is the straightforward implementation of the +-- definitional machine described in the above paper. To be precise, +-- we implement an equivalent machine, where captured continuations are +-- always sandwiched between two prompts. This equivalence as +-- well as the trick to make it all well-typed are described in +-- the FLOPS 2010 paper. Therefore, to the great extent +-- this code is the straightforward translation of delimcc from OCaml. +-- The parallel stack of delimcc is the `real' stack now (containing +-- parts of the real continuation, that is). +-- +-- This code implements, in CPS, what amounts to a segmented stack +-- (the technique of implementing call/cc efficiently, first described in +-- Hieb, Dybvig and Bruggeman's PLDI 1990 paper). +-- +module Control.CCRef (-- Types + CC, + SubCont, + Prompt, + + -- Basic delimited control operations + newPrompt, + pushPrompt, + takeSubCont, + pushSubCont, + runCC, + + -- Optimized primitives + abortP, + pushDelimSubCont, + + -- Useful derived operations + shiftP, + shift0P, + controlP, + isPromptSet, + + module Control.Mutation -- re-export + ) where + + +import Control.Monad (liftM2) +import Control.Monad.Trans +import Control.Mutation -- Generic references + +import Control.Monad.ST -- For tests only + +-- | Delimited-continuation monad transformer +-- The (CC m) monad is the Cont monad with the answer-type (), +-- combined with the persistent-state monad. The state PTop is the +-- `parallel stack' of delimcc, which is the real stack now. +-- The base monad m must support reference cells, that is, +-- be a member of the type class Mutation. +-- Since we need reference cells anyway, we represent the persistent +-- state as a reference cell PTop, which is passed as the environment. +-- +newtype CC m a = CC{unCC:: (a -> m ()) -> PTop m -> m ()} + +-- | We manipulate portions of the stack between two exception frames. +-- The type of the exception DelimCCE is () +-- +-- The type of prompts is just like that in OCaml's delimcc +data Prompt m a = Prompt{mbox :: Ref m (CC m a), + mark :: Mark m} + +-- | A frame of the parallel stack, associated with each active prompt. +-- The frame refers to the prompt indirectly, by pointing to the +-- mark field of the prompt. Different prompts have different marks. +-- Therefore, although prompts generally have different types, all pframes +-- have the same type and can be placed into the same list. +-- A pframe also points to an exception frame (in the pfr_ek field). +-- That exception frame is created by push_prompt, see below. +-- +data PFrame m = PFrame{pfr_mark :: Mark m, + pfr_ek :: EK m} -- see scAPI below + +type PStack m = [PFrame m] -- The parallel stack +type PTop m = Ref m (PStack m) -- The `machine' stack + +-- | The context between two exception frames: The captured sub-continuation +-- It is a fragment of the parallel stack: a list of PFrames in inverse order. +-- Since we are in the Cont monad, there is no `real' stack: +-- the type Ekfragment is () +-- +data SubCont m a b = SubCont{subcont_pa :: Prompt m a, + subcont_pb :: Prompt m b, + subcont_ps :: [PFrame m]} + + +-- -------------------------------------------------------------------- +-- scAPI (see the caml-shift paper) + +-- | The type of exceptions associated with exception frames +-- Only DelimCCE exceptions could ever be raised +type DelimCCE = () + +-- | The pointer to an exception frame: a continuation accepting DelimCCE +-- (since the monadic action is already a `thunk', we don't need +-- to make another one) +type EK m = m () + +{- +-- How to implement try and obtain the identity EK of the pushed +-- exception frame + +-- The code looks like call/cc, but not quite: we split the +-- machine context at the exception frame, evaluating the body in +-- essentially the empty environment. To be precise, we evaluate body +-- on the stack that contains a single underflow frame, called pop below. +-- The operation pop switches the control to the `previous' stack. + +ctry :: (Monad m, Mutation m) => (EK m -> CC m ()) -> CC m () -> CC m () +ctry body handler = CC $ \k ptop -> do + stack <- readRef ptop + let ek = unCC handler k ptop : stack + writeRef ptop ek + let pop () = do + (_:t) <- readRef ptop + writeRef ptop t + k () + unCC (body ek) pop ptop +-} + + +-- in OCaml: reset_ek : ek -> exn -> 'a +-- reset_ek :: EK m -> CC m any +-- reset_ek ek = CC $ \_ _ -> ek () + +-- | Since we are in the Cont monad, there is no `real' stack: +type Ekfragment = () +-- hence, the rest of scAPI is irrelevant: +-- copy_stack_fragment and push_stack_fragment do nothing at all + +-- -------------------------------------------------------------------- +-- | CC monad: general monadic operations +-- +instance Monad m => Monad (CC m) where + return x = CC $ \k _ -> k x + m >>= f = CC $ \k ptop -> unCC m (\v -> unCC (f v) k ptop) ptop + +instance MonadTrans CC where + lift m = CC $ \k _ -> m >>= k + +instance MonadIO m => MonadIO (CC m) where + liftIO = lift . liftIO + +runCC :: (Monad m, Mutation m) => CC m a -> m a +runCC m = do + ptop <- newRef [] -- make the parallel stack + -- where to store the answer to + ans <- newRef (error "runCC: no prompt was ever set!") + unCC m (writeRef ans) ptop + readRef ans + + +-- -------------------------------------------------------------------- +-- Utilities + +-- | Mark is Ref m Bool rather than Ref m () as was in OCaml, +-- since we use equi-mutability rather than physical equality when +-- comparing marks. Normally, mark is Ref False; we flip it to +-- True when we do the equi-mutability test. +type Mark m = Ref m Bool + +new_mark :: Mutation m => m (Mark m) +new_mark = newRef False + +-- | Do the equi-mutability test +with_marked_mark :: (Monad m, Mutation m) => Mark m -> m a -> m a +with_marked_mark mark body = do + writeRef mark True -- set the mark + r <- body + writeRef mark False -- reset it back + return r + +-- | Check if the given mark is marked +is_marked :: Mutation m => Mark m -> m Bool +is_marked = readRef + + +-- | Contents of the empty mbox +-- (see the FLOPS 2010 paper for the explanations) +mbox_empty :: CC m a +mbox_empty = error "Empty mbox" + +mbox_receive :: (Monad m, Mutation m) => Prompt m a -> CC m a +mbox_receive p = do + k <- readRef (mbox p) + writeRef (mbox p) mbox_empty + k + +-- | Operations on the global PStack +-- +push_pframe :: (Monad m, Mutation m) => PTop m -> PFrame m -> m () +push_pframe ptop fr = do + stack <- readRef ptop + writeRef ptop (fr:stack) + +pop_pframe :: (Monad m, Mutation m) => PTop m -> m (PFrame m) +pop_pframe ptop = readRef ptop >>= check + where check [] = error "Empty PStack! Can't be happening" + check (h:t) = writeRef ptop t >> return h + + +get_pstack :: (Monad m, Mutation m) => CC m (PStack m) +get_pstack = CC $ \k ptop -> readRef ptop >>= k + + +-- | Split the parallel stack at the given mark, remove the prefix +-- (up to but not including the marked frame) and return it in +-- the inverse frame order. The frame that used to be at the top of pstack +-- is now at the bottom of the returned list. +-- The other two returned values are the marked frame and the +-- rest of pstack (which contains the marked frame at the top). +-- +unwind :: (Monad m, Mutation m) => + [PFrame m] -> Mark m -> PStack m -> + m (PFrame m, PStack m, [PFrame m]) +unwind acc mark stack = with_marked_mark mark (loop acc stack) + where + loop acc [] = error "No prompt was set" + loop acc s@(h:t) = do + marked <- is_marked (pfr_mark h) + if marked then return (h,s,acc) else loop (h:acc) t + +-- | The same as above, but the removed frames are discarded +unwind_abort :: (Monad m, Mutation m) => + Mark m -> PStack m -> m (PFrame m, PStack m) +unwind_abort mark stack = with_marked_mark mark (loop stack) + where + loop [] = error "No prompt was set" + loop s@(h:t) = do + marked <- is_marked (pfr_mark h) + if marked then return (h,s) else loop t + +-- | rev_append l1 l2 == reverse l1 ++ l2 +rev_append :: [a] -> [a] -> [a] +rev_append [] l2 = l2 +rev_append (h:t) l2 = rev_append t (h:l2) + +-- -------------------------------------------------------------------- +-- | Basic Operations of the delimited control interface +-- All control operators in the end jump to the exception frame +-- +-- > (in delimcc, that was `raise DelimCCE'; here it is `pfr_ek h') +-- +newPrompt :: (Monad m, Mutation m) => CC m (Prompt m a) +newPrompt = lift $ liftM2 Prompt (newRef mbox_empty) new_mark + +-- | The exception-handling part of try in pushPrompt +popPrompt :: (Monad m, Mutation m) => + Prompt m w -> CC m w +popPrompt p = CC $ \k ptop -> do + h <- pop_pframe ptop -- remove the exception frame + -- assert (h.pfr_mark == p.mark) + unCC (mbox_receive p) k ptop + +pushPrompt :: (Monad m, Mutation m) => + Prompt m w -> CC m w -> CC m w +pushPrompt p body = CC $ \k ptop -> do + let ek = unCC (popPrompt p) k ptop + let raise = do -- raise the exception + (h:_) <- readRef ptop + pfr_ek h -- h must be an exception frame + push_pframe ptop (PFrame (mark p) ek) -- push the exception frame + unCC body (\res -> writeRef (mbox p) (return res) >> raise) ptop + + +takeSubCont :: (Monad m, Mutation m) => + Prompt m b -> (SubCont m a b -> CC m b) -> CC m a +takeSubCont p f = newPrompt >>= \pa -> CC $ \k ptop -> do + let ek = unCC (popPrompt pa) k ptop + stack <- readRef ptop + (h,s,subcontchain) <- unwind [] (mark p) (PFrame (mark pa) ek:stack) + writeRef ptop s + writeRef (mbox p) (f (SubCont pa p subcontchain)) + pfr_ek h -- reset_ek is the identity + + +pushSubCont :: (Monad m, Mutation m) => + SubCont m a b -> CC m a -> CC m b +pushSubCont (SubCont pa pb subcontchain) m = CC $ \k ptop -> do + let ek = unCC (popPrompt pb) k ptop + ephemeral <- new_mark -- p'' in the caml-shift paper + stack <- readRef ptop + let stack'@(h:_) = rev_append subcontchain (PFrame ephemeral ek:stack) + writeRef ptop stack' + writeRef (mbox pa) m + pfr_ek h -- raise the exception + + +-- | An optimization: pushing the _delimited_ continuation. +-- This is the optimization of the pattern +-- +-- > pushPrompt (subcont_pb sk) (pushSubcont sk m) +-- +-- corresponding to pushing the continuation captured by shift/shift0. +-- The latter continuation always has the delimiter at the end. +-- Indeed shift can be implemented more efficiently as a primitive +-- rather than via push_prompt/control combination... +-- +pushDelimSubCont :: (Monad m, Mutation m) => + SubCont m a b -> CC m a -> CC m b +pushDelimSubCont (SubCont pa pb subcontchain) m = CC $ \k ptop -> do + let ek = unCC (popPrompt pb) k ptop + stack <- readRef ptop + let stack'@(h:_) = rev_append subcontchain (PFrame (mark pb) ek:stack) + writeRef ptop stack' + writeRef (mbox pa) m + pfr_ek h + + +-- | An efficient variation of take_subcont, which does not capture +-- any continuation. +-- This code makes it clear that abort is essentially raise. +-- +abortP :: (Monad m, Mutation m) => + Prompt m w -> CC m w -> CC m any +abortP p res = CC $ \k ptop -> do + stack <- readRef ptop + (h,s) <- unwind_abort (mark p) stack + writeRef ptop s + writeRef (mbox p) res + pfr_ek h -- reset_ek is the identity + + +-- | Check to see if a prompt is set +isPromptSet :: (Monad m, Mutation m) => + Prompt m w -> CC m Bool +isPromptSet p = do + stack <- get_pstack + with_marked_mark (mark p) (loop stack) + where + loop [] = return False + loop s@(h:t) = do + marked <- is_marked (pfr_mark h) + if marked then return True else loop t + +-- pstack_size :: (Monad m, Mutation m) => String -> CC m () +-- pstack_size str = do +-- stack <- get_pstack +-- trace (unwords ["Pstack:",str,show (length stack)]) (return ()) + +-- -------------------------------------------------------------------- +-- | Useful derived operations +-- +shiftP :: (Monad m, Mutation m) => + Prompt m w -> ((a -> CC m w) -> CC m w) -> CC m a +shiftP p f = takeSubCont p $ \sk -> + pushPrompt p (f (\c -> + pushDelimSubCont sk (return c))) + +shift0P :: (Monad m, Mutation m) => + Prompt m w -> ((a -> CC m w) -> CC m w) -> CC m a +shift0P p f = takeSubCont p $ \sk -> + f (\c -> + pushDelimSubCont sk (return c)) + +controlP :: (Monad m, Mutation m) => + Prompt m w -> ((a -> CC m w) -> CC m w) -> CC m a +controlP p f = takeSubCont p $ \sk -> + pushPrompt p (f (\c -> + pushSubCont sk (return c))) + +---------------------------------------------------------------------- +-- Tests + +expect ve vp = if ve == vp then putStrLn $ "expected answer " ++ (show ve) + else error $ "expected " ++ (show ve) ++ + ", computed " ++ (show vp) + +assure :: Monad m => CC m Bool -> CC m () +assure m = do + v <- m + if v then return () else error "assertion failed" + + +test0 = runCC (return 1 >>= (return . (+ 4))) >>= expect 5 +-- 5 + +test1 = (expect 1 =<<) . runCC $ do + p <- newPrompt + assure (isPromptSet p >>= return . not) + pushPrompt p $ (assure (isPromptSet p) >> return 1) + +incr :: Monad m => Int -> m Int -> m Int +incr n m = m >>= return . (n +) + +test2 = (expect 9 =<<) . runCC $ do + p <- newPrompt + incr 4 . pushPrompt p $ pushPrompt p (return 5) + +test3 = (expect 9 =<<) . runCC $ do + p <- newPrompt + incr 4 . pushPrompt p $ (incr 6 $ abortP p (return 5)) + +test3' = (expect 9 =<<) . runCC $ do + p <- newPrompt + incr 4 . pushPrompt p . pushPrompt p $ (incr 6 $ abortP p (return 5)) + +-- The same, but less efficient +test3'1 = (expect 9 =<<) . runCC $ do + p <- newPrompt + incr 4 . pushPrompt p . pushPrompt p $ + (incr 6 $ takeSubCont p (\_ -> (return 5))) + +test3'' = (expect 27 =<<) . runCC $ do + p <- newPrompt + incr 20 . pushPrompt p $ + do + v1 <- pushPrompt p (incr 6 $ abortP p (return 5)) + v2 <- abortP p (return 7) + return $ v1 + v2 + 10 + +test3''1 = (expect 27 =<<) . runCC $ do + p <- newPrompt + incr 20 . pushPrompt p $ + do + v1 <- pushPrompt p (incr 6 $ takeSubCont p (\_ -> return 5)) + v2 <- takeSubCont p (\_ -> return 7) + return $ v1 + v2 + 10 + +test3''' = (print =<<) . runCC $ do + p <- newPrompt + v <- pushPrompt p $ + do + v1 <- pushPrompt p (incr 6 $ abortP p (return 5)) + v2 <- abortP p (return 7) + return $ v1 + v2 + 10 + assure (isPromptSet p >>= return . not) + v <- abortP p (return 9) + assure (return False) + return $ v + 20 +-- error + +test4 = (expect 35 =<<) . runCC $ do + p <- newPrompt + incr 20 . pushPrompt p $ + incr 10 . takeSubCont p $ \sk -> + pushPrompt p (pushSubCont sk (return 5)) + +test41 = (expect 35 =<<) . runCC $ do + p <- newPrompt + incr 20 . pushPrompt p $ + incr 10 . takeSubCont p $ \sk -> + pushSubCont sk (pushPrompt p (pushSubCont sk (abortP p (return 5)))) + + +-- Danvy/Filinski's test +--(display (+ 10 (reset (+ 2 (shift k (+ 100 (k (k 3)))))))) +--; --> 117 + +test5 = (expect 117 =<<) . runCC $ do + p <- newPrompt + incr 10 . pushPrompt p $ + incr 2 . shiftP p $ \sk -> incr 100 $ sk =<< (sk 3) +-- 117 + +test5'' = (expect 115 =<<) . runCC $ do + p0 <- newPrompt + p1 <- newPrompt + incr 10 . pushPrompt p0 $ + incr 2 . shiftP p0 $ \sk -> + incr 100 $ sk =<< + (pushPrompt p1 (incr 9 $ sk =<< (abortP p1 (return 3)))) + +test5''' = (expect 115 =<<) . runCC $ do + p0 <- newPrompt + p1 <- newPrompt + incr 10 . pushPrompt p0 $ + incr 2 . (id =<<) . shiftP p0 $ \sk -> + incr 100 $ sk + (pushPrompt p1 (incr 9 $ sk (abortP p1 (return 3)))) + +test54 = (expect 124 =<<) . runCC $ do + p0 <- newPrompt + p1 <- newPrompt + incr 10 . pushPrompt p0 $ + incr 2 . (id =<<) . shiftP p0 $ \sk -> + incr 100 $ sk + (pushPrompt p1 (incr 9 $ sk (abortP p0 (return 3)))) + +test6 = (expect 15 =<<) . runCC $ do + p1 <- newPrompt + p2 <- newPrompt + let pushtwice sk = pushSubCont sk (pushSubCont sk (return 3)) + incr 10 . pushPrompt p1 $ + incr 1 . pushPrompt p2 $ takeSubCont p1 pushtwice + +-- The most difficult test. The difference between the prompts really matters +-- now +test7 = (expect 135 =<<) . runCC $ do + p1 <- newPrompt + p2 <- newPrompt + p3 <- newPrompt + let pushtwice sk = pushSubCont sk (pushSubCont sk + (takeSubCont p2 + (\sk2 -> pushSubCont sk2 + (pushSubCont sk2 (return 3))))) + incr 100 . pushPrompt p1 $ + incr 1 . pushPrompt p2 $ + incr 10 . pushPrompt p3 $ (takeSubCont p1 pushtwice) +-- 135 + +test7' = (expect 135 =<<) . runCC $ do + p1 <- newPrompt + p2 <- newPrompt + p3 <- newPrompt + let pushtwice f = f (f (shiftP p2 (\f2 -> f2 =<< (f2 3)))) + incr 100 . pushPrompt p1 $ + incr 1 . pushPrompt p2 $ + incr 10 . pushPrompt p3 $ (shiftP p1 pushtwice >>= id) +-- 135 + +test7'' = (expect 135 =<<) . runCC $ do + p1 <- newPrompt + p2 <- newPrompt + p3 <- newPrompt + let pushtwice f = f (f (shift0P p2 (\f2 -> f2 =<< (f2 3)))) + incr 100 . pushPrompt p1 $ + incr 1 . pushPrompt p2 $ + incr 10 . pushPrompt p3 $ (shift0P p1 pushtwice >>= id) + +-- test7 in the ST monad. After all, CC is a monad transformer. +-- The only difference is the presence of runST... +test7st = runST (runCC $ do + p1 <- newPrompt + p2 <- newPrompt + p3 <- newPrompt + let pushtwice sk = pushSubCont sk (pushSubCont sk + (takeSubCont p2 + (\sk2 -> pushSubCont sk2 + (pushSubCont sk2 (return 3))))) + incr 100 . pushPrompt p1 $ + incr 1 . pushPrompt p2 $ + incr 10 . pushPrompt p3 $ (takeSubCont p1 pushtwice)) + +test7st_check = return test7st >>= expect 135 + + + +-- Checking shift, shift0, control + +testls = (expect ["a"] =<<) . runCC $ do + p <- newPrompt + pushPrompt p ( + do + let x = shiftP p (\f -> f [] >>= (return . ("a":))) + xv <- x + shiftP p (\_ -> return xv)) + + +-- (display (prompt0 (cons 'a (prompt0 (shift0 f (shift0 g '())))))) +testls0 = (expect [] =<<) . runCC $ do + p <- newPrompt + pushPrompt p ( + (return . ("a":)) =<< + (pushPrompt p (shift0P p (\_ -> (shift0P p (\_ -> return [])))))) + +testls01 = (expect ["a"] =<<) . runCC $ do + p <- newPrompt + pushPrompt p ( + (return . ("a":)) =<< + (pushPrompt p + (shift0P p (\f -> f (shift0P p (\_ -> return []))) >>= id))) + + +testlc = (expect [] =<<) . runCC $ do + p <- newPrompt + pushPrompt p ( + do + let x = controlP p (\f -> f [] >>= (return . ("a":))) + xv <- x + controlP p (\_ -> return xv)) + + +testlc' = (expect ["a"] =<<) . runCC $ do + p <- newPrompt + pushPrompt p ( + do + let x = controlP p (\f -> f [] >>= (return . ("a":))) + xv <- x + controlP p (\g -> g xv)) +-- ["a"] + +testlc1 = (expect 2 =<<) . runCC $ do + p <- newPrompt + pushPrompt p (do + takeSubCont p (\sk -> + pushPrompt p (pushSubCont sk (return 1))) + takeSubCont p (\sk -> pushSubCont sk (return 2))) + + +-- traversing puzzle by Olivier Danvy + +type DelimControl m a b = + Prompt m b -> ((a -> CC m b) -> CC m b) -> CC m a + +traverse :: Show a => DelimControl IO [a] [a] -> [a] -> IO () +traverse op lst = (print =<<) . runCC $ do + p <- newPrompt + let visit [] = return [] + visit (h:t) = do + v <- op p (\f -> f t >>= (return . (h:))) + visit v + pushPrompt p (visit lst) + + +-- *CC_Refn> traverse shiftP [1,2,3,4,5] +-- [1,2,3,4,5] +-- *CC_Refn> traverse controlP [1,2,3,4,5] +-- [5,4,3,2,1] + +doall = sequence_ [test0, test1, test2, test3, test3', test3'1, + test3'', test3''1, + test4, test41, test5, test5'', test5''', test54, + test6, test7, test7', test7'', test7st_check, + testls, testls0, testls01, testlc, testlc', testlc1 + ] +-- test3''' should raise an error diff --git a/Control/Generator1.hs b/Control/Generator1.hs new file mode 100644 --- /dev/null +++ b/Control/Generator1.hs @@ -0,0 +1,91 @@ +-- | Generators in Haskell +-- +-- We translate the in-order tree traversal example from an old article +-- Generators in Icon, Python, and Scheme, 2004. +-- +-- +-- +-- using Haskell and delimited continuations rather than call/cc + mutation. +-- The code is shorter, and it even types. +-- To be honest, we actually translate the OCaml code generator.ml +-- +-- In this code, we use a single global prompt (that is, ordinary shift0) +-- Generator2.hs shows the need for several prompts. +-- +module Control.Generator1 where + +import Control.CCExc +import Control.Monad.Trans (liftIO, lift) + +import Control.Monad.ST -- for pure tests +import Data.STRef + +{- +A sample program Python programmers seem to be proud of: an in-order +traversal of a tree: + + >>>> # A recursive generator that generates Tree leaves in in-order. + >>> def inorder(t): + ... if t: + ... for x in inorder(t.left): + ... yield x + ... yield t.label + ... for x in inorder(t.right): + ... yield x + +Given below is the complete implementation in Haskell. +-} + + +-- | A few preliminaries: define the tree and build a sample tree +-- +type Label = Int +data Tree = Leaf | Node Label Tree Tree deriving Show + +make_full_tree :: Int -> Tree +make_full_tree depth = loop 1 depth + where + loop label 0 = Leaf + loop label n = Node label (loop (2*label) (pred n)) (loop (2*label+1) (pred n)) + +tree1 = make_full_tree 3 + +-- | In Python, `yield' is a keyword. In Haskell, it is a regular function. +-- Furthermore, it is a user-defined function, in one line of code. +-- To get generators there is no need to extend a language. +-- +type P m a = PS (Res m a) -- the type of the single prompt (recursive) +newtype Res m a = Res ( (a -> CC (P m a) m ()) -> CC (P m a) m () ) +outRes body (Res f) = f body + +yield :: Monad m => a -> CC (P m a) m () +yield v = shift0P ps (\k -> return . Res $ \b -> b v >> k () >>= outRes b) + +-- | The enumerator: the for-loop essentially +enumerate iterator body = + pushPrompt ps (iterator >> (return . Res . const $ return ())) >>= + outRes body + +-- | The in_order function itself: compare with the Python version +in_order :: (Monad m) => Tree -> CC (P m Label) m () +in_order Leaf = return () +in_order (Node label left right) = do + in_order left + yield label + in_order right + +-- | Print out the result of the in-order traversal +test_io :: IO () +test_io = runCC $ enumerate (in_order tree1) (liftIO . print) + +-- 4 2 5 1 6 3 7 + +-- | Or return it as a pure list; the effects are encapsulated +test_st :: [Label] +test_st = runST (do + res <- newSTRef [] + let body v = modifySTRef res (v:) + runCC $ enumerate (in_order tree1) (lift . body) + readSTRef res >>= return . reverse) + +-- [4,2,5,1,6,3,7] diff --git a/Control/Generator2.hs b/Control/Generator2.hs new file mode 100644 --- /dev/null +++ b/Control/Generator2.hs @@ -0,0 +1,194 @@ +{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables #-} + +-- | Generators in Haskell +-- +-- We translate the in-order tree traversal example from an old article +-- Generators in Icon, Python, and Scheme, 2004. +-- +-- > http://okmij.org/ftp/Scheme/enumerators-callcc.html#Generators +-- +-- using Haskell and delimited continuations rather than call/cc + mutation. +-- The code is shorter, and it even types. +-- To be honest, we actually translate the OCaml code generator.ml +-- +-- This code is the extension of Generator1.hs; we use delimited +-- control not only to implement the generator. We also use delimited +-- control to accumulate the results in a list. We need two different +-- prompts then (with two different answer-types, as it happens). +-- This file illustrates the prompt flavors PP and PM, using newtypes +-- to define private global prompts (global prompts that are private to +-- the current module). +-- +-- +module Control.Generator2 where + +import Control.CCExc +import Control.Monad.Trans (liftIO, lift) +import Data.Typeable + +{- +A sample program Python programmers seem to be proud of: an in-order +traversal of a tree: + + >>>> # A recursive generator that generates Tree leaves in in-order. + >>> def inorder(t): + ... if t: + ... for x in inorder(t.left): + ... yield x + ... yield t.label + ... for x in inorder(t.right): + ... yield x + +Given below is the complete implementation in Haskell. +-} + + +-- | A few preliminaries: define the tree and build a sample tree +-- +type Label = Int +data Tree = Leaf | Node Label Tree Tree deriving Show + +make_full_tree :: Int -> Tree +make_full_tree depth = loop 1 depth + where + loop label 0 = Leaf + loop label n = Node label (loop (2*label) (pred n)) (loop (2*label+1) (pred n)) + +tree1 = make_full_tree 3 + +-- | In Python, `yield' is a keyword. In Haskell, it is a regular function. +-- Furthermore, it is a user-defined function, in one line of code. +-- To get generators there is no need to extend a language. +-- +-- First, we try the prompt flavor PP +-- +-- The answer-type for one of the prompts +newtype ResP m a = ResP ( (a -> CC PP m ()) -> CC PP m () ) + +instance Typeable1 m => Typeable1 (ResP m) where + typeOf1 x = mkTyConApp (mkTyCon "ResP") [m] + where m = typeOf1 (undefined:: m ()) + +outResP body (ResP f) = f body + +-- | One prompt, used by the generator (the yield/enumerate pair) +-- We instantiate the global pp to the desired answer-type. +ppy :: (Typeable1 m, Typeable a) => Prompt PP m (ResP m a) +ppy = pp + +-- | The rest of the code, up to test_io, is the same as that in Generator1.hs +yieldP :: (Typeable1 m, Typeable a) => Monad m => a -> CC PP m () +yieldP v = shift0P ppy (\k -> return . ResP $ \b -> b v >> k () >>= outResP b) + +-- | The enumerator: the for-loop essentially +enumerateP :: (Typeable1 m, Typeable a, Monad m) => + CC PP m () -> (a -> CC PP m ()) -> CC PP m () +enumerateP iterator body = + pushPrompt ppy (iterator >> (return . ResP . const $ return ())) >>= + outResP body + +-- | The in_order function itself: compare with the Python version +in_orderP :: (Typeable1 m, Monad m) => Tree -> CC PP m () +in_orderP Leaf = return () +in_orderP (Node label left right) = do + in_orderP left + yieldP label + in_orderP right + +-- | Print out the result of the in-order traversal +test_ioP :: IO () +test_ioP = runCC $ + enumerateP (in_orderP tree1) (liftIO .(print :: (Int -> IO ()))) + +-- 4 2 5 1 6 3 7 + +-- | Using the prompt flavor PM +-- +-- The above code works. We can define the second pair of operators +-- to accummulate the result into a list. Yet, the solution is +-- not very satisfactory. We notice that the prompt type ppy is +-- polymorphic over a, the elements we yield. What ensures that +-- `yieldP' yields elements of the same type that enumerateP can pass to the +-- body of the loop? Nothing, actually, at compile time. If yieldP and +-- enumerateP do not agree on the type of the elements, a run-time +-- error will occur. +-- This is where the PM prompt type comes in handy. It has a phantom +-- type parameter c, which can be used to communicate between +-- producers and consumers of the effect. We use the type parameter c +-- to communicate the type of elements, between yield and enumerate. +-- Since the parameter is phantom, it costs us nothing at run-time. +-- +-- The answer-type for one of the prompts +newtype Res m a = Res ( (a -> CC (PM a) m ()) -> CC (PM a) m () ) + +instance Typeable1 m => Typeable1 (Res m) where + typeOf1 x = mkTyConApp (mkTyCon "Res") [m] + where m = typeOf1 (undefined:: m ()) + +outRes body (Res f) = f body + +-- | One prompt, used by the generator (the yield/enumerate pair) +py :: (Typeable1 m, Typeable a) => Prompt (PM a) m (Res m a) +py = pm + +-- | The rest of the code, up to test_io, is the same as that in Generator1.hs +yield :: (Typeable1 m, Typeable a) => Monad m => a -> CC (PM a) m () +yield v = shift0P py (\k -> return . Res $ \b -> b v >> k () >>= outRes b) + +-- | The enumerator: the for-loop essentially +enumerate :: (Typeable1 m, Typeable a, Monad m) => + CC (PM a) m () -> (a -> CC (PM a) m ()) -> CC (PM a) m () +enumerate iterator body = + pushPrompt py (iterator >> (return . Res . const $ return ())) >>= + outRes body + +-- | The in_order function itself: compare with the Python version +in_order :: (Typeable1 m, Monad m) => Tree -> CC (PM Label) m () +in_order Leaf = return () +in_order (Node label left right) = do + in_order left + yield label + in_order right + +-- | Print out the result of the in-order traversal +test_io :: IO () +test_io = runCC $ enumerate (in_order tree1) (liftIO .(print :: (Int -> IO ()))) + +-- 4 2 5 1 6 3 7 + + +-- | The second application of control: accumulating the results in a list +-- +-- The answer-type for the second prompt. We use newtype for identification +newtype Acc a = Acc [a] deriving Typeable +toAcc v (Acc l) = return . Acc $ v:l + +-- | The second prompt, used by the acc/accumulated pair +-- Again we use the mark of PM to communicate the type of the elements +-- between `acc' and `accumulated'. It happens to be the same type used +-- by yield/enumetrate. +-- If that was not the case, we could have easily arranged for a type-level +-- record (see HList or the TFP paper). +pa :: (Typeable a) => Prompt (PM a) m (Acc a) +pa = pm + +acc :: (Typeable a, Monad m) => a -> CC (PM a) m () +acc v = shift0P pa (\k -> k () >>= toAcc v) + +accumulated :: (Typeable a, Monad m) => CC (PM a) m () -> CC (PM a) m [a] +accumulated body = + pushPrompt pa (body >> return (Acc [])) >>= \ (Acc l) -> return l + +test_acc :: [Label] +test_acc = runIdentity . runCC . accumulated $ + (enumerate (in_order tree1) acc) + +-- [4,2,5,1,6,3,7] + + +-- | To avoid importing mtl, we define Identity on our own +newtype Identity a = Identity{runIdentity :: a} deriving (Typeable) + +instance Monad Identity where + return = Identity + m >>= f = f $ runIdentity m diff --git a/Control/Mutation.hs b/Control/Mutation.hs new file mode 100644 --- /dev/null +++ b/Control/Mutation.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-} + +-- | This file is part of the code accompanying the paper +-- `Fun with type functions' +-- Joint work with Simon Peyton Jones and Chung-chieh Shan +-- See the paper for explanations. +-- +module Control.Mutation where + +import Data.IORef +import Data.STRef +import Control.Monad.ST +import Control.Monad.Trans + +-- | Start basic +class Mutation m where + type Ref m :: * -> * + newRef :: a -> m (Ref m a) + readRef :: Ref m a -> m a + writeRef :: Ref m a -> a -> m () + +instance Mutation IO where + type Ref IO = IORef + newRef = newIORef + readRef = readIORef + writeRef = writeIORef + +instance Mutation (ST s) where + type Ref (ST s) = STRef s + newRef = newSTRef + readRef = readSTRef + writeRef = writeSTRef +-- End basic + +-- | Start transformer +instance (Monad m, Mutation m, MonadTrans t) + => Mutation (t m) where + type Ref (t m) = Ref m + newRef = lift . newRef + readRef = lift . readRef + writeRef = (lift .) . writeRef diff --git a/Language/Fibration.lhs b/Language/Fibration.lhs new file mode 100644 --- /dev/null +++ b/Language/Fibration.lhs @@ -0,0 +1,452 @@ + [Haskell] Applicative translucent functors in Haskell + Chung-chieh Shan + Mon Sep 13 15:20:33 EDT 2004 + http://www.haskell.org/pipermail/haskell/2004-September/014515.html + Comment: added LANGUAGE pragmas. + + +On 2004-09-08T19:46:55+0200, Tomasz Zielonka wrote: + ] On Wed, Sep 08, 2004 at 04:27:23PM +0100, Simon Peyton-Jones wrote: + ]] The ML orthodoxy says that it's essential to give sharing constraints by + ]] name, not by position. If every module must be parameterised by every + ]] type it may wish to share, modules might get a tremendous number of type + ]] parameters, and matching them by position isn't robust. I think that + ]] would be the primary criticism from a programming point of view. I have + ]] no experience of how difficult this would turn out to be in practice. +] How about named fields in type constructors? Something like Haskell's +] records but at type level. Seems like a fun extension ;) + +Proponents of ML-style module systems emphasize the advantage +of `sharing by specification' (or `fibration') over `sharing by +construction' (or `parameterization') (MacQueen 1986; Pierce 2000; +Harper and Pierce 2003). As Simon Peyton-Jones noted, in the context +of our translations of ML-style modules into System F-omega and +Haskell, sharing by specification gives type-equality constraints by +name, whereas sharing by construction gives type-equality constraints +by position. Harper and Pierce (2003; Pierce 2000) give examples of +modular programming where the latter approach can lead to an exponential +number of parameters, which are clumsy to deal with at best. It has +been often suggested that records at the type level be introduced to +address this issue (Jones 1995, 1996; Shao 1999a,b; Shan 2004; Tomasz +Zielonka in this discussion thread). + +In this message, we (Oleg Kiselyov and Chung-chieh Shan) translate +Harper and Pierce's example into Haskell, using only the most common +Haskell extensions to give type-equality constraints by name and avoid +an exponential blowup. This exercise suggests that, while type-level +records may be convenient to have in Haskell, they may not be strictly +necessary to express sharing by specification. As shown below, we +can indeed refer to type parameters `by name', taking advantage of +the ability of a Haskell compiler to unify type expressions and bind +type variables. Our technique may be generalizable to encode all +sharing by specification. We hope this message helps clarify the +difference between the two sharing styles, and relate the ML and Haskell +orthodoxies. + + +First, let us demonstrate the exponential explosion of type variables. +We again will be using OCaml and Haskell in parallel, to make our +Haskell translation of module expression clearer. Later we shall +show how we prevent the exponential explosion in Ocaml -- and how +to translate that solution to Haskell. Again this message is a +doubly-literal code: both in OCaml and Haskell. It can be loaded in +GHCi or Hugs -98 as it is. To get the OCaml code, please filter the +text of the message with "sed -n -e '/^}/ s/^} //p'" + +> {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} +> {-# LANGUAGE ScopedTypeVariables #-} +> {-# LANGUAGE FunctionalDependencies #-} +> {-# LANGUAGE UndecidableInstances #-} +> module Language.Fibration where + +(The final solution arrived at by the end of this message does not +require -fallow-undecidable-instances above.) + +Let us consider a module of the following interface (a signature, in +ML speak): + +} module type FN = sig +} type a +} type b +} val app : a -> b +} end + + +This is the interface of a regular function. It can be thought of +as a compiler stage or network protocol stack that translates one +intermediate language or representation (type a) into another (type b). +Here are two sample modules of that signature: + +} module TIF = struct +} type a = int +} type b = float +} let app x = float_of_int x +} end +} +} module TFI = struct +} type a = float +} type b = int +} let app x = truncate x + 1 +} end + + +In our Haskell translation, a signature corresponds to a type class, +and an implementation (a structure, aka module) to an instance: + +> class NFN a b where +> napp:: a -> b +> +> instance NFN Integer Float where +> napp x = fromInteger x +> +> instance NFN Float Integer where +> napp x = truncate x + 1 + +Let us write a module that represents a composition appr . appl of +two FN-functions: appl: al->bl and appr: ar->br. In order for the +composition to be well-formed, the result type of appl must be the +argument type of appr: bl = ar (which we will call the intermediate +type t). Let us further suppose that we wish to make this intermediate +type explicit (e.g., for inspection, to resolve overloading, to invoke +the two intermediate functions separately, etc). Thus we arrive at the +following interface: + +} module type NFN1 = sig +} type a1 +} type t +} type b1 +} val app1 : a1 -> b1 +} end + +Or, in Haskell + +> class NFN1 a t b where +> napp1:: t -> a -> b + +Note that the type of the intermediate result is really needed in +Haskell, to resolve the overloading and properly select the instance. + + +The composition of two modules of the signature FN is computed by the +following transparent functor: + +} module NFn1(L: FN)(R: (FN with type a = L.b)) = struct +} type a1 = L.a +} type t = L.b +} type b1 = R.b +} let app1 x = R.app (L.app x) +} end + +It takes two modules of the signature FN, labeled L and R. We should +note a _sharing constraint_: the type a of module R must be the same +as the type b of module L. The result of the NFn1 is a module of the +signature NFN1. + +Here is an example of using the module + +} module TIFI = NFn1(TIF)(TFI) +} let test_tifi = TIFI.app1 7;; (* 8 *) + + +In Haskell, the functor corresponds to an instance with constraints +that correspond to the argument signatures. The sharing is expressed +by sharing of the names of type variables: + +> instance (NFN a t, NFN t b) => NFN1 a t b where +> napp1 t x = napp (napp x `asTypeOf` t) +> +> test_nfn1::Integer +> test_nfn1 = napp1 (undefined::Float) (7::Integer) -- 8 + +Suppose we wish to compose two modules NFN1 again. Again, we wish to +expose all intermediate types + +} module type NFN2 = sig +} type a2 +} type tl type t type tr +} type b2 +} val app2 : a2 -> b2 +} end +} +} module NFn2(L: NFN1)(R: (NFN1 with type a1 = L.b1)) = struct +} type a2 = L.a1 +} type tl = L.t +} type t = L.b1 +} type tr = R.t +} type b2 = R.b1 +} let app2 x = R.app1 (L.app1 x) +} end + + +We should note again that the functor NFn2 imports two modules of the +signature NFN1 and re-exports their types, after relabeling them to avoid +ambiguity and applying the sharing constraint R.a1 = L.b1. + +In Haskell: + +> class NFN2 a tl t tr b where +> napp2:: (tl,t,tr) -> a -> b +> +> instance (NFN1 a tl t, NFN1 t tr b) => NFN2 a tl t tr b where +> napp2 (tl,t,tr) x = napp1 tr $ ((napp1 tl x) `asTypeOf` t) + +We can do that again: + +} module type NFN3 = sig +} type a3 +} type tl type t type tr +} type b3 +} val app3 : a3 -> b3 +} end +} +} module NFn3(L: NFN2)(R: (NFN2 with type a2 = L.b2)) = struct +} type a3 = L.a2 +} type tll = L.tl +} type tl = L.t +} type trl = L.tr +} type t = L.b2 +} type tlr = R.tl +} type tr = R.t +} type trr = R.tr +} type b3 = R.b2 +} let app3 x = R.app2 (L.app2 x) +} end + + +In Haskell: + +> class NFN3 a tll tl tlr t trl tr trr b where +> napp3:: ((tll,tl,tlr),t,(trl,tr,trr)) -> a -> b +> +> instance (NFN2 a tll tl tlr t, NFN2 t trl tr trr b) +> => NFN3 a tll tl tlr t trl tr trr b where +> napp3 (tl,t,tr) x = napp2 tr $ ((napp2 tl x) `asTypeOf` t) + +Here is a usage example + +} module TII = struct +} type a = int +} type b = int +} let app x = x + 2 +} end +} +} module NM1 = NFn1(TII)(TII) +} module NM2 = NFn2(NM1)(NM1) +} module NM3 = NFn3(NM2)(NM2) +} let test_nm3 = NM3.app3 5;; (* 21 *) + + +> instance NFN Integer Integer where +> napp x = x + 2 +> +> test_nfn3:: Integer +> test_nfn3 = let i = undefined::Integer +> i3 = (i,i,i) +> in napp3 (i3,i,i3) (5::Integer) -- 21 + +The exponential explosion of the type variables is apparent. The term +expressions, the module expressions, and the sharing constraints are all +`linear'. That is, if we wish to define another level of composition, +NFN4, we write an expression similar to NFn3, which, if we disregard the +type variables, has roughly the same size, in characters. It's only +when we look at the type variables we see the explosion. The explosion +can be overcome if could magically say: import module NFNn as L; import +module NFNn as R; make sure that L.bn = R.an; and re-export the rest. +Alas, we can't deal with the type variables of a structure 'in bulk'. +If we wish to re-export them, we have to enumerate them all. + +The explosion is particularly apparent in Haskell, where we refer to +type parameters of a class by their position rather than by their name. +If we wish to write another level of composition, say, NFN4, we merely +need the first type variable NFN3 and the last type variable of NFN3. +Alas, we have to enumerate all the type variables in-between. + + +It turns out that we _can_ refer to type variables of a module `in bulk', +both in OCaml and in Haskell. To do that, we introduce a more +structural representation: + +} module type FN1 = sig +} type a type b type t +} module ML : (FN with type a = a and type b = t) +} module MR : (FN with type b = b and type a = t) +} val app : a -> b +} end +} +} module Fn1(L: FN)(R: (FN with type a = L.b)) = struct +} type a = L.a type b = R.b type t = L.b +} module ML = L module MR = R +} let app x = R.app (L.app x) +} end +} +} module type FN2 = sig +} type a type b type t +} module ML : (FN1 with type a = a and type b = t) +} module MR : (FN1 with type b = b and type a = t) +} val app : a -> b +} end +} +} module Fn2(L: FN1)(R: (FN1 with type a = L.b)) = struct +} type a = L.a type b = R.b type t = L.b +} module ML = L module MR = R +} let app x = R.app (L.app x) +} end + + +The details of the two halves of the composition are stowed away in the +submodules ML and MR. We avoid the explosion in Ocaml because we can +mention, for example, the type tl in NFN2 above as ML.t in FN2 instead. +We can build a chain of functions using source code of size logarithmic +in the length of the chain. + +Let us extend the chain one more time for illustration, and show an +example: + +} module type FN3 = sig +} type a type b type t +} module ML : (FN2 with type a = a and type b = t) +} module MR : (FN2 with type b = b and type a = t) +} val app : a -> b +} end +} +} module Fn3(L: FN2)(R: (FN2 with type a = L.b)) = struct +} type a = L.a type b = R.b type t = L.b +} module ML = L module MR = R +} let app x = R.app (L.app x) +} end +} +} module M1 = Fn1(TIF)(TFI) +} module M2 = Fn2(M1)(M1) +} module M3 = Fn3(M2)(M2) +} let test_m3 = M3.app 5;; (* 9 *) + + +With the help of Haskell type classes, we can also stow away the +detailed type information of a module. + +First, we re-define our class representing the signature FN to take an +extra type parameter: + +> class FN s a b | s -> a, s -> b where +> app:: s -> a -> b + +The parameter 's' is a `label' that uniquely identifies an instance of +the class FN: in other words, the label 's' represents a module of a +signature FN. The label is a `proxy' for the module. Here are a few +examples of such modules: + +> instance FN (Integer->Float) Integer Float where +> app _ x = fromInteger x +> +> instance FN (Float->Integer) Float Integer where +> app _ x = truncate x + 1 +> +> instance FN (Integer->Integer) Integer Integer where +> app _ x = x + 2 +> +> data L = L +> instance FN L Integer Integer where +> app _ x = x + 2 + +In the last example, we used an `artificial' label `L'. Now we can +write the signature and the functor FN1 that `composes' FN once, the +signature FN2 and the corresponding functor that compose FN twice, +etc. However, because in Haskell an instance can refer to itself, we +can create a recursive functor and a signature: + +> instance (FN u a t, FN v t b) => FN (u,v) a b where +> app s = app (snd s) . app (fst s) + +The FN instance above subsumes the old classes NFN1, NFN2, NFN3, etc., +all under the same FN class: + +> fn'1 = undefined :: (Integer->Float, Float->Integer) +> fn'2 = (fn'1, fn'1) +> fn'3 = (fn'2, fn'2) +> test_fn' = app fn'3 5 -- 9 + + +If fn'1 is a 2-stage compiler, then fn'2 is a 4-stage compiler and +fn'3 is an 8-stage one. The types of fn'1, fn'2, fn'3 above grow +exponentially, just as the Ocaml signature FN2 above is twice the size +of FN1 when expanded out. But signature definitions in Ocaml and type +synonyms in Haskell allow us to avoid the explosion in the source code. + +Even though the details of these composed modules are stowed away, +they are not hidden. Indeed, the label uniquely determines the the +module. We can inspect the label or its type to find sub-labels, +which uniquely describe the intermediate modules and their internal +types. For example, here is a Haskell function that runs the first 3 +stages of an 8-stage compiler like fn'3: + +> stages123of8 ~((s12,(s3,s4)),s5678) +> = app s3 . app s12 + +The type of stages123of8 is inferred to be + *Fibration> :t stages123of8 + stages123of8 :: forall b a s5678 s4 s3 s12 b1. + (FN s12 a b1, FN s3 b1 b) => + ((s12, (s3, s4)), s5678) -> a -> b + +Here ((s12,(s3,s4)),s5678) is a dummy type argument that identifies the +module (in other words, resolves the overloading). Note that the term +and type above only mentions the parts of the module that are actually +used, not the exponentially-sized details of say s5678. We thus avoid +exponential blowup and achieve sharing by specification. + +> test_stagem3 = stages123of8 fn'3 5 + + *Fibration> :t test_stagem3 + test_stagem3 :: Float + *Fibration> test_stagem3 + 6.0 + +We should point out that we have indeed accessed an intermediate type in +fn'3: although the whole compiler "app fn'3" maps Integer to Integer, +the first three stages map Integer to an intermediate type Float. We +have taken a great advantage of the pattern-matching ability of the +Haskell compiler: the ability to unify one type expression with the +other and bind type variables. + + +REFERENCES + +Robert Harper, and Benjamin C. Pierce. 2003. Design issues in advanced +module systems. In Advanced topics in types and programming languages, +ed. Benjamin C. Pierce. Cambridge: MIT Press. Draft manuscript. + +Mark P. Jones. 1995. From Hindley-Milner types to first-class structures. +In Proceedings of the Haskell workshop, ed. Paul Hudak. Tech. Rep. YALEU/ +DCS/RR-1075, New Haven: Department of Computer Science, Yale University. +http://www.cse.ogi.edu/~mpj/pubs/haskwork95.pdf + +Mark P. Jones. 1996. Using parameterized signatures to express modular +structure. In POPL '96: Conference record of the annual ACM symposium +on principles of programming languages, 68-78. New York: ACM Press. +http://www.cse.ogi.edu/~mpj/pubs/paramsig.html +http://www.cse.ogi.edu/~mpj/pubs/paramsig.pdf + +David B. MacQueen. 1986. Using dependent types to express modular +structure. In POPL '86: Conference record of the annual ACM symposium +on principles of programming languages, 277-286. New York: ACM Press. +http://www.cs.bell-labs.com/who/dbm/papers/popl86/paper.ps + +Benjamin C. Pierce. 2000. Advanced module systems: A guide for the +perplexed. ICFP invited talk. +http://www.cis.upenn.edu/~bcpierce/papers/modules-icfp.ps + +Chung-chieh Shan. 2004. Higher-order modules in System F-omega and +Haskell. Draft manuscript. +http://www.cs.rutgers.edu/~ccshan/xlate/xlate.pdf + +Zhong Shao. 1999a. Transparent modules with fully syntactic signatures. +In ICFP '99: Proceedings of the ACM international conference on functional +programming, vol. 34(9) of ACM SIGPLAN Notices, 220-232. New York: +ACM Press. +http://flint.cs.yale.edu/flint/publications/fullsig.pdf + +Zhong Shao. 1999b. Transparent modules with fully syntactic signatures. +Tech. Rep. YALEU/ DCS/ TR-1181, Department of Computer Science, Yale +University, New Haven. +http://flint.cs.yale.edu/flint/publications/fullsig-tr.pdf + diff --git a/liboleg.cabal b/liboleg.cabal --- a/liboleg.cabal +++ b/liboleg.cabal @@ -1,5 +1,5 @@ name: liboleg -version: 2010.1.7.1 +version: 2010.1.9.0 license: BSD3 license-file: LICENSE author: Oleg Kiselyov @@ -39,6 +39,13 @@ Control.Poly2 Control.StateAlgebra + Control.CCExc + Control.CCCxe + Control.CCRef + Control.Mutation + Control.Generator1 + Control.Generator2 + Codec.Image.Tiff Lambda.CCG @@ -83,6 +90,7 @@ Language.ToTDPE Language.Typ Language.TypeCheck + Language.Fibration Logic.DynEpistemology