[Haskell-cafe] Re: Control.Monad.Cont fun
Hi, Sorry, I have to do a small correction to an earlier post of mine. On 7/9/05, I wrote: In order to move the function (\jmp - jmp `runC` jmp) into callCC, the following law, that all instances of MonadCont seem to satisfy, is very helpful. f = callCC g === callCC (\k - f = g ((=) k . f)) This law is in fact only satisfied for some monads (QuickCheck suggests Cont r and ContT r m). A counterexample for the reader transfomer: type M = ReaderT Bool (Cont Bool) f :: a - M Bool f _ = ask g :: (Bool - M a) - M a g k = local not $ k True run :: M Bool - Bool run (ReaderT m) = m True `runCont` id Now, run (f = callCC g) == True run (callCC (\k - f = g ((=) k . f))) == False In particular (regarding Functor as superclass of Monad), it follows f `fmap` callCC g === callCC (\k - f `fmap` g (k . f)) This law (the one I actually used) is satisfied (again, only according to QuickCheck) by every monad I checked. Thomas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Monad.Cont fun
Hi Thomas and Tomasz, A late comment about a MonadFix instance for Cont/ContT: Thomas Jäger wrote: Hello Tomasz, This stuff is very interesting! At first sight, your definition of getCC seems quite odd, but it can in fact be derived from its implementation in an untyped language. On 7/7/05, Tomasz Zielonka [EMAIL PROTECTED] wrote: ... Besides sharing my happiness, I want to ask some questions: - is it possible to define a MonadFix instance for Cont / ContT? It must be possible to define something that looks like a MonadFix instance, after all you can define generally recursive functions in languages like scheme and sml which live in a ContT r IO monad, but this has all kinds of nasty consequences, iirc. Levent Erkök's thesis suggests (pp. 66) that there's no implementation of mfix that satisfies the purity law. http://www.cse.ogi.edu/PacSoft/projects/rmb/erkok-thesis.pdf A while ago, I attempted to marry value recursion a la Levent Erkök with the continuation-monad transformer. It seems possible if the underlying monad has value recursion and references. Interestingly, all mfix properties except left shrinking appear to be valid. There are slides about this (including implementation) at http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf There is also a draft paper at http://www.cse.ogi.edu/~magnus/mdo-callcc.pdf I should warn that the paper is still very unfinished. If anyone is interested in picking up the pieces together with me, please get in touch! Cheers, Magnus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Monad.Cont fun
Tomasz Zielonka wrote: On Fri, Jul 15, 2005 at 11:51:59PM +0200, Magnus Carlsson wrote: A while ago, I attempted to marry value recursion a la Levent Erkök with the continuation-monad transformer. It seems possible if the underlying monad has value recursion and references. Interestingly, all mfix properties except left shrinking appear to be valid. There are slides about this (including implementation) at http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf There is also a draft paper at http://www.cse.ogi.edu/~magnus/mdo-callcc.pdf I've already found your paper and played with the implementation :-) :-) I was stupid to think that with MonadCont+MonadFix+getCC it would be possible to do forward jumps, but of course it doesn't work because of the strictness law. I would expect forward jumps to work. For example, consider callcc (\k - mfix (\v - E)) where we assume that E is an expression in which k and v are free. Then it would be OK for E to invoke k and thereby jump forward. In this case, the recursive value (bound to v) is simply bottom. Moreover, suppose E in turn captures the current continuation and gives it as an argument to k. Then, it is possible to jump back inside E again at a later point. E might in this case return a non-bottom value, which also would be the value of v. Cheers, Magnus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Monad.Cont fun
On Fri, Jul 15, 2005 at 11:51:59PM +0200, Magnus Carlsson wrote: A while ago, I attempted to marry value recursion a la Levent Erkök with the continuation-monad transformer. It seems possible if the underlying monad has value recursion and references. Interestingly, all mfix properties except left shrinking appear to be valid. There are slides about this (including implementation) at http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf There is also a draft paper at http://www.cse.ogi.edu/~magnus/mdo-callcc.pdf I've already found your paper and played with the implementation :-) I was stupid to think that with MonadCont+MonadFix+getCC it would be possible to do forward jumps, but of course it doesn't work because of the strictness law. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Control.Monad.Cont fun
On Sat, Jul 09, 2005 at 07:05:20PM +0200, Thomas Jäger wrote:
Hello Tomasz,
Hello Thomas,
Haskell doesn't support infinite types, but we can get close enough by
creating a type C m b such that C m b and C m b - m b become
isomorphic:
newtype C m b = C { runC :: C m b - m b }
Thanks for this tip - I am sure it will help me in the future.
With the help of C we can implement another version of getCC and
rewrite the original example.
[...]
We can move the self-application of jmp into getCC to get the same
type signature as your solution, but we still rely on the auxiliary
datatype C.
[...]
It is easy to get rid of C here arriving exactly at your definition of getCC.
Neat! I didn't know (or didn't thought about) how to systematically
derive getCC. Thanks!
- is it possible to define a MonadFix instance for Cont / ContT?
Levent Erkök's thesis suggests (pp. 66) that there's no implementation
of mfix that satisfies the purity law.
http://www.cse.ogi.edu/PacSoft/projects/rmb/erkok-thesis.pdf
This is a very interesting reading.
- do you think it would be a good idea to add them to
Control.Monad.Cont?
I think so, because they simplify the use of continuations in an
imperative setting and are probably helpful in understanding
continuations. Letting continuations escape is quite a common pattern
in scheme code, and painful to do in Haskell without your cool trick.
I'll try to come up with some motivating examples, unless someone who
is in power to add these functions is reading this thread and agrees
that they are useful... ?
Alternatively, we could place them on http://haskell.org/hawiki/MonadCont.
Wow! I noticed there is a link to my message already ;-)
Best regards
Tomasz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Control.Monad.Cont fun
Hello Tomasz,
This stuff is very interesting! At first sight, your definition of
getCC seems quite odd, but it can in fact be derived from its
implementation in an untyped language.
On 7/7/05, Tomasz Zielonka [EMAIL PROTECTED] wrote:
Some time ago I wanted to return the escape continuation out of the
callCC block, like this:
getCC = callCC (\c - return c)
We get the error message
test124.hs:8:29:
Occurs check: cannot construct the infinite type: t = t - t1
Expected type: t - t1
Inferred type: (t - t1) - m b
Haskell doesn't support infinite types, but we can get close enough by
creating a type C m b such that C m b and C m b - m b become
isomorphic:
newtype C m b = C { runC :: C m b - m b }
With the help of C we can implement another version of getCC and
rewrite the original example.
getCC1 :: (MonadCont m) = m (C m b)
getCC1 = callCC $ \k - return (C k)
test1 :: ContT r IO ()
test1 = do
jmp - getCC1
liftIO $ putStrLn hello1
jmp `runC` jmp -- throw the continuation itself,
-- so we can jump to the same point the next time.
return ()
We can move the self-application of jmp into getCC to get the same
type signature as your solution, but we still rely on the auxiliary
datatype C.
getCC2 :: MonadCont m = m (m b)
getCC2 = do
jmp - callCC $ \k - return (C k)
return $ jmp `runC` jmp
In order to move the function (\jmp - jmp `runC` jmp) into callCC,
the following law, that all instances of MonadCont seem to satisfy, is
very helpful.
f = callCC g === callCC (\k - f = g ((=) k . f))
In particular (regarding Functor as superclass of Monad), it follows
f `fmap` callCC g === callCC (\k - f `fmap` g (k . f))
Therefore, getCC2 is equivalent to
getCC3 :: MonadCont m = m (m b)
getCC3 = callCC $ \k - return (selfApp $ C (k . selfApp)) where
selfApp :: C m b - m b
selfApp jmp = jmp `runC` jmp
It is easy to get rid of C here arriving exactly at your definition of getCC.
getCC :: MonadCont m = m (m a)
getCC = callCC (\c - let x = c x in return x)
getCC' :: MonadCont m = a - m (a, a - m b)
getCC' x0 = callCC (\c - let f x = c (x, f) in return (x0, f))
For what it's worth, this can be derived in much the same way from the
(not well-typed)
getCC' x = callCC $ \k - return (k, x)
using the auxillary type
newtype C' m a b = C' { runC' :: (C' m a b, a) - m b }
Besides sharing my happiness, I want to ask some questions:
- is it possible to define a MonadFix instance for Cont / ContT?
It must be possible to define something that looks like a MonadFix
instance, after all you can define generally recursive functions in
languages like scheme and sml which live in a ContT r IO monad, but
this has all kinds of nasty consequences, iirc.
Levent Erkök's thesis suggests (pp. 66) that there's no implementation
of mfix that satisfies the purity law.
http://www.cse.ogi.edu/PacSoft/projects/rmb/erkok-thesis.pdf
- do you think it would be a good idea to add them to
Control.Monad.Cont?
I think so, because they simplify the use of continuations in an
imperative setting and are probably helpful in understanding
continuations. Letting continuations escape is quite a common pattern
in scheme code, and painful to do in Haskell without your cool trick.
I'd also like to have shift and reset functions there :)
Best wishes,
Thomas
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Control.Monad.Cont fun
On Thu, Jul 07, 2005 at 06:02:36PM -0700, [EMAIL PROTECTED] wrote: Delimited continuations are really cool. Thanks for the pointer. I am reading the paper by Dybvig, Jones and Sabry right now. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Control.Monad.Cont fun
Tomasz Zielonka wrote: Some time ago I wanted to return the escape continuation out of the callCC block, like this: getCC = callCC (\c - return c) patterns like this are characteristic of shift/reset -- From http://www.haskell.org/hawiki/MonadCont reset :: (Monad m) = ContT a m a - ContT r m a reset e = ContT $ \k - runContT e return = k shift :: (Monad m) = ((a - ContT r m b) - ContT b m b) - ContT b m a shift e = ContT $ \k - runContT (e $ \v - ContT $ \c - k v = c) return with them, we can implement the same tests, in a slightly de-sugared way, for clarity: newtype H r m = H (H r m - ContT r m r) unH (H x) = x -- prints hello! in an endless loop test :: IO () test = (`runContT` return) $ reset (do jump - shift (\f - f (H f)) lift (putStrLn hello!) unH jump jump) newtype H' r m a = H' ((a,H' r m a) - ContT r m ()) unH' (H' x) = x -- prints integers from 0 to 10, then prints finish and ends test' :: IO () test' = (`runContT` return) $ do reset (do (x, jumpWith) - (\x - shift (\f - f (x,(H' f 0 lift (print x) when (x 10) (unH' jumpWith ((x + 1),jumpWith))) lift (putStrLn finish) Delimited continuations are really cool. The lack of the answer-type polymorphism in ContT will come to bite us in the end: we can't use reset several times in differently-typed contexts (which often means that we can use reset only once in our program). The CC monad transformer (derived from the CC library by Sabry, Dybvig, Peyton-Jones), freely available from http://pobox.com/~oleg/ftp/packages/LogicT.tar.gz is free from that drawback. BTW, with that monad transformer, the example looks as follows (again, in a de-sugared way, for clarity) import CC_2CPST newtype H'' r m a = H'' (CC r m (a,H'' r m a) - CC r m ()) unH'' (H'' x) = x test'' :: IO () test'' = runCC ( do p - newPrompt pushPrompt p ( do (x, jumpWith) - (\x - shiftP p (\f - f (return (x,(H'' f) 0 lift (print x) when (x 10) (unH'' jumpWith (return ((x + 1),jumpWith lift (putStrLn finish)) shiftP p f = letSubCont p $ \sk - pushPrompt p (f (\c - pushPrompt p (pushSubCont sk c))) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
