liboleg 2010.1.7.1 → 2010.1.9.0
raw patch · 8 files changed
+1924/−1 lines, 8 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Control.CCCxe: abortP :: (Monad m) => Prompt p m w -> CC p m w -> CC p m any
+ Control.CCCxe: as_prompt_type :: Prompt p m w -> w -> Prompt p m w
+ Control.CCCxe: controlP :: (Monad m) => Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
+ Control.CCCxe: data CC p m a
+ Control.CCCxe: data P2 w1 w2 m x
+ Control.CCCxe: data PD m x
+ Control.CCCxe: data PM c m x
+ Control.CCCxe: data PP m x
+ Control.CCCxe: data PS w m x
+ Control.CCCxe: instance (Monad m) => Monad (CC p m)
+ Control.CCCxe: instance (MonadIO m) => MonadIO (CC p m)
+ Control.CCCxe: instance MonadTrans (CC p)
+ Control.CCCxe: newPrompt :: (Typeable w) => Int -> Prompt PD m w
+ Control.CCCxe: p2L :: Prompt (P2 w1 w2) m w1
+ Control.CCCxe: p2R :: Prompt (P2 w1 w2) m w2
+ Control.CCCxe: pm :: (Typeable w) => Prompt (PM c) m w
+ Control.CCCxe: pp :: (Typeable w) => Prompt PP m w
+ Control.CCCxe: ps :: Prompt (PS w) m w
+ Control.CCCxe: pushPrompt :: (Monad m) => Prompt p m w -> CC p m w -> CC p m w
+ Control.CCCxe: pushSubCont :: (Monad m) => SubCont p m a b -> CC p m a -> CC p m b
+ Control.CCCxe: runCC :: (Monad m) => CC (p :: (* -> *) -> * -> *) m a -> m a
+ Control.CCCxe: shift0P :: (Monad m) => Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
+ Control.CCCxe: shiftP :: (Monad m) => Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
+ Control.CCCxe: takeSubCont :: (Monad m) => Prompt p m w -> CCT p m x w -> CC p m x
+ Control.CCCxe: type CCT p m a w = SubCont p m a w -> CC p m w
+ Control.CCCxe: 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))
+ Control.CCCxe: type SubCont p m a b = CC p m a -> CC p m b
+ Control.CCExc: abortP :: (Monad m) => Prompt p m w -> CC p m w -> CC p m any
+ Control.CCExc: as_prompt_type :: Prompt p m w -> w -> Prompt p m w
+ Control.CCExc: controlP :: (Monad m) => Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
+ Control.CCExc: data CC p m a
+ Control.CCExc: data P2 w1 w2 m x
+ Control.CCExc: data PD m x
+ Control.CCExc: data PM c m x
+ Control.CCExc: data PP m x
+ Control.CCExc: data PS w m x
+ Control.CCExc: instance (Monad m) => Monad (CC p m)
+ Control.CCExc: instance (MonadIO m) => MonadIO (CC p m)
+ Control.CCExc: instance MonadTrans (CC p)
+ Control.CCExc: newPrompt :: (Typeable w) => Int -> Prompt PD m w
+ Control.CCExc: p2L :: Prompt (P2 w1 w2) m w1
+ Control.CCExc: p2R :: Prompt (P2 w1 w2) m w2
+ Control.CCExc: pm :: (Typeable w) => Prompt (PM c) m w
+ Control.CCExc: pp :: (Typeable w) => Prompt PP m w
+ Control.CCExc: ps :: Prompt (PS w) m w
+ Control.CCExc: pushPrompt :: (Monad m) => Prompt p m w -> CC p m w -> CC p m w
+ Control.CCExc: pushSubCont :: (Monad m) => SubCont p m a b -> CC p m a -> CC p m b
+ Control.CCExc: runCC :: (Monad m) => CC (p :: (* -> *) -> * -> *) m a -> m a
+ Control.CCExc: shift0P :: (Monad m) => Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
+ Control.CCExc: shiftP :: (Monad m) => Prompt p m w -> ((a -> CC p m w) -> CC p m w) -> CC p m a
+ Control.CCExc: takeSubCont :: (Monad m) => Prompt p m w -> CCT p m x w -> CC p m x
+ Control.CCExc: type CCT p m a w = SubCont p m a w -> CC p m w
+ Control.CCExc: 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))
+ Control.CCExc: type SubCont p m a b = CC p m a -> CC p m b
+ Control.CCRef: abortP :: (Monad m, Mutation m) => Prompt m w -> CC m w -> CC m any
+ Control.CCRef: controlP :: (Monad m, Mutation m) => Prompt m w -> ((a -> CC m w) -> CC m w) -> CC m a
+ Control.CCRef: data CC m a
+ Control.CCRef: data Prompt m a
+ Control.CCRef: data SubCont m a b
+ Control.CCRef: instance (Monad m) => Monad (CC m)
+ Control.CCRef: instance (MonadIO m) => MonadIO (CC m)
+ Control.CCRef: instance MonadTrans CC
+ Control.CCRef: isPromptSet :: (Monad m, Mutation m) => Prompt m w -> CC m Bool
+ Control.CCRef: newPrompt :: (Monad m, Mutation m) => CC m (Prompt m a)
+ Control.CCRef: pushDelimSubCont :: (Monad m, Mutation m) => SubCont m a b -> CC m a -> CC m b
+ Control.CCRef: pushPrompt :: (Monad m, Mutation m) => Prompt m w -> CC m w -> CC m w
+ Control.CCRef: pushSubCont :: (Monad m, Mutation m) => SubCont m a b -> CC m a -> CC m b
+ Control.CCRef: runCC :: (Monad m, Mutation m) => CC m a -> m a
+ Control.CCRef: shift0P :: (Monad m, Mutation m) => Prompt m w -> ((a -> CC m w) -> CC m w) -> CC m a
+ Control.CCRef: shiftP :: (Monad m, Mutation m) => Prompt m w -> ((a -> CC m w) -> CC m w) -> CC m a
+ Control.CCRef: takeSubCont :: (Monad m, Mutation m) => Prompt m b -> (SubCont m a b -> CC m b) -> CC m a
+ Control.Generator1: Leaf :: Tree
+ Control.Generator1: Node :: Label -> Tree -> Tree -> Tree
+ Control.Generator1: Res :: ((a -> CC (P m a) m ()) -> CC (P m a) m ()) -> Res m a
+ Control.Generator1: data Tree
+ Control.Generator1: in_order :: (Monad m) => Tree -> CC (P m Label) m ()
+ Control.Generator1: instance Show Tree
+ Control.Generator1: make_full_tree :: Int -> Tree
+ Control.Generator1: newtype Res m a
+ Control.Generator1: test_io :: IO ()
+ Control.Generator1: test_st :: [Label]
+ Control.Generator1: type Label = Int
+ Control.Generator1: type P m a = PS (Res m a)
+ Control.Generator1: yield :: (Monad m) => a -> CC (P m a) m ()
+ Control.Generator2: Acc :: [a] -> Acc a
+ Control.Generator2: Identity :: a -> Identity a
+ Control.Generator2: Leaf :: Tree
+ Control.Generator2: Node :: Label -> Tree -> Tree -> Tree
+ Control.Generator2: Res :: ((a -> CC (PM a) m ()) -> CC (PM a) m ()) -> Res m a
+ Control.Generator2: ResP :: ((a -> CC PP m ()) -> CC PP m ()) -> ResP m a
+ Control.Generator2: acc :: (Typeable a, Monad m) => a -> CC (PM a) m ()
+ Control.Generator2: accumulated :: (Typeable a, Monad m) => CC (PM a) m () -> CC (PM a) m [a]
+ Control.Generator2: data Tree
+ Control.Generator2: enumerate :: (Typeable1 m, Typeable a, Monad m) => CC (PM a) m () -> (a -> CC (PM a) m ()) -> CC (PM a) m ()
+ Control.Generator2: enumerateP :: (Typeable1 m, Typeable a, Monad m) => CC PP m () -> (a -> CC PP m ()) -> CC PP m ()
+ Control.Generator2: in_order :: (Typeable1 m, Monad m) => Tree -> CC (PM Label) m ()
+ Control.Generator2: in_orderP :: (Typeable1 m, Monad m) => Tree -> CC PP m ()
+ Control.Generator2: instance (Typeable1 m) => Typeable1 (Res m)
+ Control.Generator2: instance (Typeable1 m) => Typeable1 (ResP m)
+ Control.Generator2: instance Monad Identity
+ Control.Generator2: instance Show Tree
+ Control.Generator2: instance Typeable1 Acc
+ Control.Generator2: instance Typeable1 Identity
+ Control.Generator2: make_full_tree :: Int -> Tree
+ Control.Generator2: newtype Acc a
+ Control.Generator2: newtype Identity a
+ Control.Generator2: newtype Res m a
+ Control.Generator2: newtype ResP m a
+ Control.Generator2: pa :: (Typeable a) => Prompt (PM a) m (Acc a)
+ Control.Generator2: ppy :: (Typeable1 m, Typeable a) => Prompt PP m (ResP m a)
+ Control.Generator2: py :: (Typeable1 m, Typeable a) => Prompt (PM a) m (Res m a)
+ Control.Generator2: runIdentity :: Identity a -> a
+ Control.Generator2: test_acc :: [Label]
+ Control.Generator2: test_io :: IO ()
+ Control.Generator2: test_ioP :: IO ()
+ Control.Generator2: type Label = Int
+ Control.Generator2: yield :: (Typeable1 m, Typeable a) => (Monad m) => a -> CC (PM a) m ()
+ Control.Generator2: yieldP :: (Typeable1 m, Typeable a) => (Monad m) => a -> CC PP m ()
+ Control.Mutation: class Mutation m where { type family Ref m :: * -> *; }
+ Control.Mutation: instance (Monad m, Mutation m, MonadTrans t) => Mutation (t m)
+ Control.Mutation: instance Mutation (ST s)
+ Control.Mutation: instance Mutation IO
+ Control.Mutation: newRef :: (Mutation m) => a -> m (Ref m a)
+ Control.Mutation: readRef :: (Mutation m) => Ref m a -> m a
+ Control.Mutation: writeRef :: (Mutation m) => Ref m a -> a -> m ()
+ Language.Fibration: L :: L
+ Language.Fibration: app :: (FN s a b) => s -> a -> b
+ Language.Fibration: class FN s a b | s -> a, s -> b
+ Language.Fibration: class NFN a b
+ Language.Fibration: class NFN1 a t b
+ Language.Fibration: class NFN2 a tl t tr b
+ Language.Fibration: class NFN3 a tll tl tlr t trl tr trr b
+ Language.Fibration: data L
+ Language.Fibration: instance (FN u a t, FN v t b) => FN (u, v) a b
+ Language.Fibration: instance (NFN a t, NFN t b) => NFN1 a t b
+ Language.Fibration: instance (NFN1 a tl t, NFN1 t tr b) => NFN2 a tl t tr b
+ Language.Fibration: instance (NFN2 a tll tl tlr t, NFN2 t trl tr trr b) => NFN3 a tll tl tlr t trl tr trr b
+ Language.Fibration: instance FN (Float -> Integer) Float Integer
+ Language.Fibration: instance FN (Integer -> Float) Integer Float
+ Language.Fibration: instance FN (Integer -> Integer) Integer Integer
+ Language.Fibration: instance FN L Integer Integer
+ Language.Fibration: instance NFN Float Integer
+ Language.Fibration: instance NFN Integer Float
+ Language.Fibration: instance NFN Integer Integer
+ Language.Fibration: napp :: (NFN a b) => a -> b
+ Language.Fibration: napp1 :: (NFN1 a t b) => t -> a -> b
+ Language.Fibration: napp2 :: (NFN2 a tl t tr b) => (tl, t, tr) -> a -> b
+ Language.Fibration: napp3 :: (NFN3 a tll tl tlr t trl tr trr b) => ((tll, tl, tlr), t, (trl, tr, trr)) -> a -> b
+ Language.Fibration: test_nfn1 :: Integer
+ Language.Fibration: test_nfn3 :: Integer
Files
- Control/CCCxe.hs +251/−0
- Control/CCExc.hs +258/−0
- Control/CCRef.hs +628/−0
- Control/Generator1.hs +91/−0
- Control/Generator2.hs +194/−0
- Control/Mutation.hs +41/−0
- Language/Fibration.lhs +452/−0
- liboleg.cabal +9/−1
+ Control/CCCxe.hs view
@@ -0,0 +1,251 @@+{-# LANGUAGE PatternGuards, KindSignatures #-}+{-# LANGUAGE ExistentialQuantification, RankNTypes, ImpredicativeTypes #-}++-- This file is the CPS version of CCExc.hs, implementing the identical+-- interface+--+-- <http://okmij.org/ftp/continuations/implementations.html#CC-monads>+--+-- 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
+ Control/CCExc.hs view
@@ -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+--+-- <http://okmij.org/ftp/continuations/implementations.html#CC-monads>+--+-- > 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 <http://okmij.org/ftp/gengo/CAG-talk.pdf>+-- 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
+ Control/CCRef.hs view
@@ -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
+ Control/Generator1.hs view
@@ -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.+--+-- <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+--+-- 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]
+ Control/Generator2.hs view
@@ -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
+ Control/Mutation.hs view
@@ -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
+ Language/Fibration.lhs view
@@ -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+
liboleg.cabal view
@@ -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