[Haskell-cafe] Re: An interesting monad: Prompt
Felipe Lessa wrote: Ryan Ingram wrote: [snip] data Prompt (p :: * - *) :: (* - *) where PromptDone :: result - Prompt p result -- a is the type needed to continue the computation Prompt :: p a - (a - Prompt p result) - Prompt p result [snip] runPromptM :: Monad m = (forall a. p a - m a) - Prompt p r - m r runPromptM _ (PromptDone r) = return r runPromptM f (Prompt pa c) = f pa = runPromptM f . c [snip] How can we prove that (runPromptM prompt === id)? I was trying to go with You probably mean runPromptM id = id runPromptM prompt (PromptDone r) = return r = PromptDone r runPromptM prompt (Prompt pa c) = prompt pa = runPromptM prompt . c = Prompt pa return = runPromptM prompt . c = Prompt pa ((= (runPromptM prompt . c) . return) = Prompt pa (runPromptM prompt . c) and I got stuck here. It seems obvious that we can strip out the 'runPromptM prompt' down there to finish the proof, but that doesn't sound very nice, as I'd need to suppose what I'm trying to prove. Am I missing something here? You want to deduce runPromptM id (Prompt pa c) = Prompt pa c from runPromptM id (Prompt pa c) = Prompt pa (runPromptM id . c) by somehow assuming that runPromptM id = id at least when applied to c . If it were a problem about lists like foldr (:) [] = id you could use mathematical induction . You can do the same here, but you need to use coinduction. For more, see also http://www.cs.nott.ac.uk/~gmh/bib.html#corecursion Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: An interesting monad: Prompt
On Jan 4, 2008 9:59 AM, apfelmus [EMAIL PROTECTED] wrote: Felipe Lessa wrote: How can we prove that (runPromptM prompt === id)? I was trying to go with You probably mean runPromptM id = id Actually, I meant an specialization of 'runPromptM prompt': runPromptM id :: (Monad p) = Prompt p r - p r runPromptM prompt :: (MonadPrompt p m) = Prompt p r - m r runPromptM (prompt :: p a - Prompt p a) :: Prompt p r - Prompt p r [snip] you could use mathematical induction . You can do the same here, but you need to use coinduction. For more, see also http://www.cs.nott.ac.uk/~gmh/bib.html#corecursion Thanks for the tip! So I can define approx :: Integer - Prompt p r - Prompt p r approx (n+1) (PromptDone r) = PromptDone r approx (n+1) (Prompt p c) = Prompt p (approx n . c) runId :: Prompt p r - Prompt p r runId = runPromptM prompt and try to prove that ∀n. approx n (id x) == approx n (runId x) We can see trivially that approx n (id (PromptDone r)) == approx n (runId (PromptDone r)) For the case that x is (Prompt p c), we'll prove using induction. The base case n = 0 is trivially proven as ∀x. approx 0 x == ⊥. For the indutive case, approx (m+1) (runId (Prompt p c)) -- definition of runId = approx (m+1) (runPromptM prompt (Prompt p c)) -- definition of runPromptM for the Prompt case = approx (m+1) (prompt p = runPromptM prompt . c) -- definition of prompt in the Prompt instance = approx (m+1) (Prompt p return = runPromptM prompt . c) -- definition of (=) in the Prompt instance = approx (m+1) (Prompt p ((= runPromptM prompt . c) . return)) -- monad law '(return x = f) == f x' = approx (m+1) (Prompt p (runPromptM prompt . c)) -- definition of approx = Prompt p (approx m . runPromptM prompt . c) -- definition of runId = Prompt p (approx m . runId . c) -- definition of (.) twice = Prompt p (\x - approx m (runId (c x))) -- induction hypothesis = Prompt p (\x - approx m (id (c x)) -- definition of (.) twice = Prompt p (approx m . id . c) -- definition of approx = approx (m+1) (Prompt p (id . c)) -- law 'id . f == f' = approx (m+1) (Prompt p c) -- law 'x == id x' = approx (m+1) (id (Prompt p c)) Which was to be proven. ∎ I think I didn't commit any mistake above =). Thanks again for help, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: An interesting monad: Prompt
Derek Elkins wrote:
Ryan Ingram wrote:
apfelmus wrote:
A context passing implementation (yielding the ContT monad
transformer)
will remedy this.
Wait, are you saying that if you apply ContT to any monad that has the
left recursion on = takes quadratic time problem, and represent
all primitive operations via lift (never using = within lift),
that you will get a new monad that doesn't have that problem?
If so, that's pretty cool.
To be clear, by ContT I mean this monad:
newtype ContT m a = ContT { runContT :: forall b. (a - m b) - m b }
instance Monad m = Monad (ContT m) where
return x = ContT $ \c - c x
m = f = ContT $ \c - runContT m $ \a - runContT (f a) c
fail = lift . fail
instance MonadTrans ContT where
lift m = ContT $ \c - m = c
evalContT :: Monad m = ContT m a - m a
evalContT m = runContT m return
Yes, that's the case because the only way to use = from the old monad
is via lift. Since only primitive operations are being lifted into the
left of =, it's only nested in a right-associative fashion. The
remaining thing to prove is that ContT itself doesn't have the
left-associativity problem or any other similar problem. It's pretty
intuitive, but unfortunately, I currently don't know how to prove or
even specify that exactly. The problem is that expressions with =
contain arbitrary unapplied lambda abstractions and mixed types but the
types shouldn't be much a minor problem.
Indeed this was discussed on #haskell a few weeks ago. That information
has been put on the wiki at
http://www.haskell.org/haskellwiki/Performance/Monads
and refers to a blog post http://r6.ca/blog/20071028T162529Z.html that
describes it in action.
Note that the crux of the Maybe example on the wiki page is not curing a
left-associativity problem, Maybe doesn't have one. The key point here
is that continuation passing style allows us to inline the liftings
(Just x =) = \f - f x
(Nothing =) = \_ - Nothing
and thus eliminate lots of case analysis. (Btw, this is exactly the
behavior of exceptions in an imperative language.)
(Concerning the blog post, it looks like this inlining brings speed. But
Data.Sequence is not to be underestimated, it may well be responsible
for the meat of the speedup.)
I'm fairly confident, though I'd have to actually work through it, that
the Unimo work, http://web.cecs.pdx.edu/~cklin/ could benefit from
this. In fact, I think this does much of what Unimo does and could
capture many of the same things.
Well, Unimo doesn't have the left-associativity problem in the first
place, so the only motive for using ContT Prompt instead is to
eliminate the Bind constructor and implied case analyses.
But there's a slight yet important difference between Unimo p a and
Unimo' p a = ContT (Prompt p) a , namely the ability the run the
continuation in the outer monad. Let me explain: in the original
Unimo, we have a helper function
observe_monad :: (a - v)
- (forall b . p (Unimo p) b - (b - Unimo p a) - v)
- (Unimo p a - v)
for running a monad. For simplicity and to match with Ryan's prompt,
we'll drop the fact that p can be parametrized on the outer monad,
i.e. we consider
observe_monad :: (a - v)
- (forall b . p b - (b - Unimo p a) - v)
- (Unimo p a - v)
This is just the case expression for the data type
data PromptU p a where
Return :: a - PromptU p a
BindEffect :: p b - (b - Unimo p a) - PromptU p a
observe_monad :: (PromptU p a - v) - (Unimo p a - v)
The difference I'm after is that the second argument to BindEffect is
free to return an Unimo and not only another PromptU! This is quite
handy for writing monads.
In contrast, things for Unimo' p a = ContT (Prompt p) a are as follows:
data Prompt p a where
Return :: a - Prompt p a
BindEffect :: p b - (b - Prompt p a) - Prompt p a
observe :: (Prompt p a - v) - (Unimo' p a - v)
observe f m = f (runCont m Return)
Here, we don't have access to the outer monad Unimo' p a when
defining an argument f to observe. I don't think we can fix that by
allowing the second argument of BindEffect to return an Unimo' p a
since in this case,
lift :: p a - Unimo' p a
lift x = Cont $ BindEffect x
won't work anymore.
Of course, the question now is whether this can be fixed. Put
differently, this is the question I keep asking: does it allow Unimo
to implement strictly more monads than ContT = Unimo' or is the latter
enough? I.e. can every monad be implemented with ContT?
Regards,
apfelmus
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: An interesting monad: Prompt
On Sat, 2007-11-24 at 11:10 +0100, apfelmus wrote:
Derek Elkins wrote:
Ryan Ingram wrote:
apfelmus wrote:
A context passing implementation (yielding the ContT monad
transformer)
will remedy this.
Wait, are you saying that if you apply ContT to any monad that has the
left recursion on = takes quadratic time problem, and represent
all primitive operations via lift (never using = within lift),
that you will get a new monad that doesn't have that problem?
If so, that's pretty cool.
To be clear, by ContT I mean this monad:
newtype ContT m a = ContT { runContT :: forall b. (a - m b) - m b }
instance Monad m = Monad (ContT m) where
return x = ContT $ \c - c x
m = f = ContT $ \c - runContT m $ \a - runContT (f a) c
fail = lift . fail
instance MonadTrans ContT where
lift m = ContT $ \c - m = c
evalContT :: Monad m = ContT m a - m a
evalContT m = runContT m return
Yes, that's the case because the only way to use = from the old monad
is via lift. Since only primitive operations are being lifted into the
left of =, it's only nested in a right-associative fashion. The
remaining thing to prove is that ContT itself doesn't have the
left-associativity problem or any other similar problem. It's pretty
intuitive, but unfortunately, I currently don't know how to prove or
even specify that exactly. The problem is that expressions with =
contain arbitrary unapplied lambda abstractions and mixed types but the
types shouldn't be much a minor problem.
Indeed this was discussed on #haskell a few weeks ago. That information
has been put on the wiki at
http://www.haskell.org/haskellwiki/Performance/Monads
and refers to a blog post http://r6.ca/blog/20071028T162529Z.html that
describes it in action.
Note that the crux of the Maybe example on the wiki page is not curing a
left-associativity problem, Maybe doesn't have one.
I agree, hence the fact that that is massively understated. However,
while Maybe may not have a problem on the same order, there is
definitely a potential inefficiency.
(Nothing = f) = g expands to
case (case Nothing of Nothing - Nothing; Just x - f x) of
Nothing - Nothing
Just y - g y
This tests that original Nothing twice. This can be arbitrarily deep.
The right associative version would expand to
case Nothing of
Nothing - Nothing
Just x - f x = g
The key point here
is that continuation passing style allows us to inline the liftings
(Just x =) = \f - f x
(Nothing =) = \_ - Nothing
and thus eliminate lots of case analysis. (Btw, this is exactly the
behavior of exceptions in an imperative language.)
Indeed, avoiding case analyses and achieving exactly the behaviour of
exceptions was the motivation.
(Concerning the blog post, it looks like this inlining brings speed. But
Data.Sequence is not to be underestimated, it may well be responsible
for the meat of the speedup.)
I'm not quite sure what all is being compared to what, but Russell
O'Connor did say that using continuations passing style did lead to a
significant percentage speed up.
I'm fairly confident, though I'd have to actually work through it, that
the Unimo work, http://web.cecs.pdx.edu/~cklin/ could benefit from
this. In fact, I think this does much of what Unimo does and could
capture many of the same things.
Well, Unimo doesn't have the left-associativity problem in the first
place, so the only motive for using ContT Prompt instead is to
eliminate the Bind constructor and implied case analyses.
But there's a slight yet important difference between Unimo p a and
Unimo' p a = ContT (Prompt p) a , namely the ability the run the
continuation in the outer monad. Let me explain: in the original
Unimo, we have a helper function
observe_monad :: (a - v)
- (forall b . p (Unimo p) b - (b - Unimo p a) - v)
- (Unimo p a - v)
for running a monad. For simplicity and to match with Ryan's prompt,
we'll drop the fact that p can be parametrized on the outer monad,
i.e. we consider
observe_monad :: (a - v)
- (forall b . p b - (b - Unimo p a) - v)
- (Unimo p a - v)
This is just the case expression for the data type
data PromptU p a where
Return :: a - PromptU p a
BindEffect :: p b - (b - Unimo p a) - PromptU p a
observe_monad :: (PromptU p a - v) - (Unimo p a - v)
The difference I'm after is that the second argument to BindEffect is
free to return an Unimo and not only another PromptU! This is quite
handy for writing monads.
In contrast, things for Unimo' p a = ContT (Prompt p) a are as follows:
data Prompt p a where
Return :: a - Prompt p a
BindEffect :: p b - (b - Prompt p a) - Prompt p a
observe :: (Prompt p a - v) - (Unimo' p a - v)
observe f m = f (runCont m Return)
Re: [Haskell-cafe] Re: An interesting monad: Prompt
On 11/22/07, apfelmus [EMAIL PROTECTED] wrote:
A context passing implementation (yielding the ContT monad transformer)
will remedy this.
Wait, are you saying that if you apply ContT to any monad that has the left
recursion on = takes quadratic time problem, and represent all primitive
operations via lift (never using = within lift), that you will get a new
monad that doesn't have that problem?
If so, that's pretty cool.
To be clear, by ContT I mean this monad:
newtype ContT m a = ContT { runContT :: forall b. (a - m b) - m b }
instance Monad m = Monad (ContT m) where
return x = ContT $ \c - c x
m = f = ContT $ \c - runContT m $ \a - runContT (f a) c
fail = lift . fail
instance MonadTrans ContT where
lift m = ContT $ \c - m = c
evalContT :: Monad m = ContT m a - m a
evalContT m = runContT m return
-- ryan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: An interesting monad: Prompt
On Fri, 2007-11-23 at 21:11 -0800, Ryan Ingram wrote:
On 11/22/07, apfelmus [EMAIL PROTECTED] wrote:
A context passing implementation (yielding the ContT monad
transformer)
will remedy this.
Wait, are you saying that if you apply ContT to any monad that has the
left recursion on = takes quadratic time problem, and represent
all primitive operations via lift (never using = within lift),
that you will get a new monad that doesn't have that problem?
If so, that's pretty cool.
To be clear, by ContT I mean this monad:
newtype ContT m a = ContT { runContT :: forall b. (a - m b) - m b }
instance Monad m = Monad (ContT m) where
return x = ContT $ \c - c x
m = f = ContT $ \c - runContT m $ \a - runContT (f a) c
fail = lift . fail
instance MonadTrans ContT where
lift m = ContT $ \c - m = c
evalContT :: Monad m = ContT m a - m a
evalContT m = runContT m return
Indeed this was discussed on #haskell a few weeks ago. That information
has been put on the wiki at
http://www.haskell.org/haskellwiki/Performance/Monads
and refers to a blog post http://r6.ca/blog/20071028T162529Z.html that
describes it in action.
I'm fairly confident, though I'd have to actually work through it, that
the Unimo work, http://web.cecs.pdx.edu/~cklin/ could benefit from
this. In fact, I think this does much of what Unimo does and could
capture many of the same things.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: An interesting monad: Prompt
Ryan Ingram wrote: I've been trying to implement a few rules-driven board/card games in Haskell and I always run into the ugly problem of how do I get user input? The usual technique is to embed the game in the IO Monad: The problem with this approach is that now arbitrary IO computations are expressible as part of a game action, which makes it much harder to implement things like replay, undo, and especially testing! The goal was to be able to write code like this: ] takeTurn :: Player - Game () ] takeTurn player = do ] piece - action (ChoosePiece player) ] attack - action (ChooseAttack player piece) ] bonusTurn - executeAttack piece attack ] when bonusTurn $ takeTurn player but be able to script the code for testing, allow undo, automatically be able to save replays, etc. While thinking about this problem earlier this week, I came up with the following solution: class Monad m = MonadPrompt p m | m - p where prompt :: p a - m a prompt is an action that takes a prompt type and gives you a result. A simple example: ] prompt [1,3,5] :: MonadPrompt [] m = m Int This prompt would ask for someone to pick a value from the list and return it. This would be somewhat useful on its own; you could implement a choose function that picked randomly from a list of options and gave non-deterministic (or even exhaustive) testing, but on its own this wouldn't be much better than the list monad. [...] data Prompt (p :: * - *) :: (* - *) where PromptDone :: result - Prompt p result -- a is the type needed to continue the computation Prompt :: p a - (a - Prompt p result) - Prompt p result Intuitively, a (Prompt p result) either gives you an immediate result (PromptDone), or gives you a prompt which you need to reply to in order to continue the computation. This type is a MonadPrompt: instance Functor (Prompt p) where fmap f (PromptDone r) = PromptDone (f r) fmap f (Prompt p cont) = Prompt p (fmap f . cont) instance Monad (Prompt p) where return = PromptDone PromptDone r = f = f r Prompt p cont = f = Prompt p ((= f) . cont) instance MonadPrompt p (Prompt p) where prompt p = Prompt p return Marvelous! Basically, by making the continuation (a - Prompt p result) explicit, we have the flexibility to acquire the value a differently, like through user input or a replay script. The popular continuations for implementing web applications in Lisp/Scheme do the same thing. A slightly different point of view is that you use a term implementation for your monad, at least for the interesting primitive effects like choosePiece :: Player - Game Piece chooseAttack :: Player - Piece - Game Attack By using constructors for them, you have the flexibility to write different interpreters for Game a , like play :: Game a - IO a replay :: Game a - GameScript - a with the semantics play (choosePiece pl = f) = do putStrLn Player ++ show pl ++ , choose your piece: play f . read = getLine replay (choosePiece pl = f) (Piece pl' piece:xs) | pl == pl' = replay (f piece) xs Just for the record, the most general term implementation is presented here Chuan-kai Lin. Programming Monads Operationally with Unimo. http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf Btw, the web framework WASH/CGI for Haskell uses some kind of prompt monad, too. Peter Thiemann. An Embedded Domain-Specific Language for Type-Safe Server-Side Web-Scripting. http://www.informatik.uni-freiburg.de/~thiemann/WASH/draft.pdf Here, the server replays parts of the CGI monad when the user submits a form i.e. answers to a prompt. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: An interesting monad: Prompt
On 11/21/07, apfelmus [EMAIL PROTECTED] wrote: A slightly different point of view is that you use a term implementation for your monad, at least for the interesting primitive effects That's a really interesting point of view, which had struck me slightly, but putting it quite clearly like that definitely helps me understand what is going on. In fact, it seems like I can implement the original list and state examples from the Unimo paper in terms of Prompt as well, using a specialized observation function. For example: data StateP s a where Get :: StateP s s Put :: s - StateP s () runStateP :: Prompt (StateP s) a - s - (a,s) runStateP (PromptDone a) s = (a,s) runStateP (Prompt Get k) s = runStateP (k s) s runStateP (Prompt (Put s) k) _ = runStateP (k ()) s instance MonadState s (Prompt (StatePrompt s)) where get = prompt Get put = prompt . Put Strangely, this makes me less happy about Prompt rather than more; if it's capable of representing any reasonable computation, it means it's not really the targeted silver bullet I was hoping for. On the other hand, it still seems useful for what I am doing. I definitely feel like the full term implementation (like the Unimo paper describes) is overkill; unless I'm misunderstanding what's going on there, you're basically destroying any ability for the compiler to reason about your computations by reifying them into data. As long as (=) and return are functions that get inlined, lots of extraneous computation can be eliminated as the compiler discovers the monad laws through compile-time beta-reduction; once you turn them into data constructors that ability basically goes away. That said, the generalization to monad transformers and the metaprogramming techniques demonstrated look pretty cool. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
