[Haskell-cafe] comprehending monad execution

[rick at rickmurphy.org]

All:

I've been analyzing monads for a while now and have a question on execution. I suspect I've missed something basic.

In the snippet below the ghc debugger shows that in just one single step Discriminate has been substituted for g.
Even with :trace turned on in the debugger there is no evidence of an execution step to carry out the substitution.
This leads me to assume a compile time operation identifies Discriminate as a substitute for g.

Could someone correct my assumption or explain how this works?

Note: this snippet was extracted from [1].

> {-# LANGUAGE EmptyDataDecls, Rank2Types #-}
> module LEM where
> import Control.Monad.Identity
>
> data F -- no constructors
>
> data Discriminate a b = L a | R b
> instance Monad (Discriminate e) where
> return = R
> R x >>= f = f x
> L x >>= f = L x
>
> h :: (forall m. Monad m => ((a -> m F) -> m F)) -> a
> h g = case g (\x -> L x) of
> R x -> error "Not reachable"
> L x -> x
>
> -- A proof term for a -> NOT NOT a
> lift :: forall a m. Monad m => a -> ((a -> m F) -> m F)
> lift x = \k -> k x
>
> t = h $ lift True 
>

ghci trace ...

C:\haskell\lem>ghci lem.lhs
GHCi, version 6.8.3: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling LEM ( lem.lhs, interpreted )
Ok, modules loaded: LEM.
*LEM> :b h
Breakpoint 0 activated at lem.lhs:(14,2)-(16,17)
*LEM> :trace t
Loading package mtl-1.1.0.1 ... linking ... done.
Stopped at lem.lhs:(14,2)-(16,17)
_result :: a = _
[lem.lhs:(14,2)-(16,17)] *LEM> :step
Stopped at lem.lhs:(14,8)-(16,17)
_result :: a = _
g :: (a -> Discriminate a F) -> Discriminate a F = _
[lem.lhs:(14,8)-(16,17)] *LEM> :hist
-1 : h (lem.lhs:(14,2)-(16,17))
-2 : t (lem.lhs:22:6-18)
<end of history>
[lem.lhs:(14,8)-(16,17)] *LEM>


My previous analysis includes running single step execution on Wadler's I monad here [2], 
where I am able to observe execution of the I monad.

[essence.lhs:32:33-37] *Essence> :hist
-1 : unitI (essence.lhs:7:34)
-2 : unitI (essence.lhs:7:2-34)
-3 : interp (essence.lhs:32:26-38)
-4 : interp (essence.lhs:(31,2)-(39,44))
-5 : test (essence.lhs:54:41-51)
-6 : showval (essence.lhs:(26,2)-(28,45))
-7 : showI (essence.lhs:9:34-42)
-8 : showI (essence.lhs:9:2-42)
-9 : test (essence.lhs:54:34-52)
-10 : test (essence.lhs:54:2-52)
<end of history>

[1] http://okmij.org/ftp/Computation/lem.html
[2] http://homepages.inf.ed.ac.uk/wadler/papers/essence/essence.ps

Thanks much in advance for your help.

Rick



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100511/5d5c3f66/attachment.html