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
