state in the continuation monad...
I am trying to model state in the continuation monad, such that each continuation recieves the current state as one of its arguments. The state must vary in type, which is why I am trying to use the continuation monad, but things don't seem to be going too well. To clarify... imagine the following sequence: do cont1 cont2 cont3 we may want the implicit parameter for cont1 to be an Int, but for it to pass a String to cont2 which passes (String,Int) to cont3 which finally returns something else. so: is it possible to write cont1 etc... ? can anybody tell me what its type would be? Keean.
{-# OPTIONS -fglasgow-exts #-} {- Regarding Keean's posting ... I wonder whether perhaps a more basic step is to understand how type-changing monadic computations can be understood. By this I mean, that the effects model by the monad can change their type as part of the computation. Such a monad would be parameterised by effect types a b, where a is the type of the effect before computation and b is the type after computation. The following code illustrates this idea. Ralf Warm-up: we compute a normal sequence of monadic ticks, and we get back the final state and the value of the computation. ghci6.2> ticks (3,2) Demo: we do the same with heterogeneous monadic operations, and we get back the type-level natural for the final state etc. ghci6.2> hTicks (HSucc (HSucc (HSucc HZero)),2) -} ----------------------------------------------------------------------------- -- Value-level (i.e., normal) state monads ---------------------------------- ----------------------------------------------------------------------------- -- A silly state monad data State s a = State (s -> (s,a)) unState (State f) = f instance Monad (State s) where return a = State (\s -> (s,a)) c >>= f = State (\s -> let (s',a) = unState c s in unState (f a) s' ) -- Start with state 0 runZero :: State Int a -> (Int,a) runZero f = unState f 0 -- Tick and return original value tick :: State Int Int tick = State (\s -> (s+1,s)) -- Do a sequence of computations ticks = runZero ( tick >>= const tick >>= const tick) ----------------------------------------------------------------------------- -- Now in a type-driven fashion --------------------------------------------- ----------------------------------------------------------------------------- -- A state monad with type-changing states data HState s s' a = HState (s -> (s',a)) unHState (HState f) = f -- A class for heterogeneous returns class HReturn m x where hReturn :: a -> m x x a instance HReturn HState s where hReturn a = HState (unState (return a)) -- A class for heterogeneous binds class HBind m x y z where hBind :: m x y a -> (a -> m y z b) -> m x z b instance HBind HState x y z where c `hBind` f = HState (\s -> let (s',a) = unHState c s in unHState (f a) s' ) -- We use type-level naturals for different state types data HZero = HZero deriving Show data HSucc x = HSucc x deriving Show class HNat x where hNat :: x -> Int instance HNat HZero where hNat HZero = 0 instance HNat n => HNat (HSucc n) where hNat (HSucc n) = 1 + hNat n -- Start with state HZero runHZero :: HState HZero n a -> (n,a) runHZero f = unHState f HZero -- Tick and return original value htick :: HNat n => HState n (HSucc n) Int htick = HState (\s -> (HSucc s,hNat s)) -- Do a sequence of computations hTicks = runHZero ( htick `hBind` const htick `hBind` const htick) -- Should print: ((3,2),(HSucc (HSucc (HSucc HZero)),2)) main = print (ticks,hTicks)
On 2004-07-02T16:15:15+0200, Ralf Laemmel wrote:
I wonder whether perhaps a more basic step is to understand how type-changing monadic computations can be understood. By this I mean, that the effects model by the monad can change their type as part of the computation. Such a monad would be parameterised by effect types a b, where a is the type of the effect before computation and b is the type after computation.
A monad on a category C is a monoid in the category of endofunctors on C. Dylan Thurston, who knows more category theory than I do, tells me that a monoid in a category D is a D-enriched category with a single object. Hence a monad on a category C is a single-object category enriched by the category of endofunctors on C. If we remove the single-object restriction, we arrive at a generalization of monads: a category enriched by the category of endofunctors on C. I call this an efect on C, where "efect" stands for "endofunctor-enriched category". Intuitively, each object in an efect is a state, and each morphism a transition, in a directed graph. For example, a file may be open or closed, and can only be accessed while open. That'd be a two-state efect. John Power, who knows way more category theory than I do, tells me that an enriched category is much nicer (i.e., it actually helps to be an enriched category) when the enriching category is closed. I wonder how this statement plays out in the case of efects. The state monad is one example of a monad that can be generalized to an efect. The continuation monad can also be generalized to an efect; indeed, Danvy and Filinski did so in 1989 when they gave a type system for the delimited control operators shift and reset that allows the answer type to change during a computation (DIKU technical report 89/12; http://www.daimi.au.dk/~danvy/Papers/fatc.ps.gz). Just as the state monad can be implemented with the continuation monad, the state efect can be implemented with the continuation efect. I wonder whether Filinski's representation of monads in terms of shift and reset (POPL 1994, 1999; CMU dissertation 1996) generalizes to efects. That is, can any efect be implemented with the continuation efect? More pragmatically important perhaps, how can we make efects at least as easy to use and understand as monads by the practical programmer? -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig It is dry and hot, but cloudy, in Phnom Penh, Cambodia Do Ken. Ken Do Ken Do. Do Ken Do Ken Do Ken Do. Ken. Do. Ken. "The following ballot is for voting on a General Resolution to address the effect of the previous general resolution." - Debian Project Secretary
participants (3)
-
Chung-chieh Shan -
MR K P SCHUPKE -
Ralf Laemmel