[Haskell-cafe] Can every monad can be implemented with Cont? (was: New slogan for haskell.org)
Don Stewart wrote: allbery: Didn't someone already prove all monads can be implemented in terms of Cont? Cont and StateT, wasn't it? And the schemers have no choice about running in StateT :) You sure? I want to see the proof :) Last time I stumbled upon something like this, the proof was to embed every monad m in the type type Cont m a = forall b . (a - m b) - m b with an instance Monad (Cont m) where ... _independent_ of whether m is a monad or not. The problem I see with it is that we didn't really encode m with it since we're still dependent on return and (=) via project :: Monad m = Cont m a - m a project f = f return and inject :: Monad m = m a - Cont m a inject x = (x =) I mean, the starting point for a concrete monad M are some primitive operations like get :: M s put :: s - M () and a function observe :: M a - (S - (a,S)) together with laws for the primitive operations (= operational semantics) observe (put s = x) = \_ - observe (x ()) s observe (get = x) = \s - observe (x s ) s and for return observe (return a)= \s - (a,s) Now, implementing a monad means to come up with a type M and functions (=) and return that fulfill the monad laws. (In general, the result type of observe is _not_ M a !) This can be done with the standard trick of implementing stuff as constructors (see Unimo for details http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf). But - and that's the problem - I don't see how it can be done with Cont in all cases. It works for the above state monad (*) but what about primitives like mplus :: m a - m a - m a callcc :: ((a - m r) - m r) - m a that have monadic arguments in a contravariant position (possibly even universally quantified)? Regards, apfelmus *: Here you go: type Observe s a = s - (a,s) type State s a = Cont (Observe s) a get = \x - (\s - observe (x s ) s) -- law for get put s = \x - (\_ - observe (x ()) s) -- law for put observe f = f $ \a - (\s - (a,s)) -- law for observe (return a) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can every monad can be implemented with Cont? (was: New slogan for haskell.org)
Hello, Didn't someone already prove all monads can be implemented in terms of Cont? Cont and StateT, wasn't it? And the schemers have no choice about running in StateT :) You sure? I want to see the proof :) I think this is referring to Andrzej Filinski's paper Representing Layered Monads in which it shown that stacks of monads can be implemented directly (no layering) by using call/cc and mutable state. -Jeff ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can every monad can be implemented with Cont? (was: New slogan for haskell.org)
jeff p wrote: I think this is referring to Andrzej Filinski's paper Representing Layered Monads in which it shown that stacks of monads can be implemented directly (no layering) by using call/cc and mutable state. I have been unable to see how to bring its crucial reify and reflect to Haskell. In particular reflect: reflect :: m a - a It looks very magical. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can every monad can be implemented with Cont? (was: New slogan for haskell.org)
On Saturday 13 October 2007, Albert Y. C. Lai wrote: jeff p wrote: I think this is referring to Andrzej Filinski's paper Representing Layered Monads in which it shown that stacks of monads can be implemented directly (no layering) by using call/cc and mutable state. I have been unable to see how to bring its crucial reify and reflect to Haskell. In particular reflect: reflect :: m a - a It looks very magical. Here: http://cs.ioc.ee/mpc-amast06/msfp/filinski-slides.pdf are some slides Filinski made about doing monadic reflection in Haskell (there might be a corresponding paper, but a cursory googling didn't find it). The thing is, 'reflect' in Haskell doesn't have type 'm a - a' It has type something like: m a - ContState a However, in the languages he usually works with, everything is already implicitly in a ContState monad, in that they have mutable references and native continuations. Hence the type 'm a - a' there. At least, I think that's the explanation. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
