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