[Haskell-cafe] state in the continuation monad...

[Ralf Laemmel]

-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}

{-

Regarding Keean's posting ...
I wonder whether perhaps a more basic step is to understand
how type-changing monadic computations can be understood.
By this I mean, that the effects model by the monad can change
their type as part of the computation. Such a monad would be
parameterised by effect types a b, where a is the type of the
effect before computation and b is the type after computation.

The following code illustrates this idea.

Ralf


Warm-up: we compute a normal sequence of monadic ticks,
and we get back the final state and the value of the computation.

ghci6.2> ticks
         (3,2)

Demo: we do the same with heterogeneous monadic operations,
and we get back the type-level natural for the final state etc.

ghci6.2> hTicks
         (HSucc (HSucc (HSucc HZero)),2)

-}


-----------------------------------------------------------------------------
-- Value-level (i.e., normal) state monads ----------------------------------
-----------------------------------------------------------------------------

-- A silly state monad
data State s a = State (s -> (s,a))
unState (State f) = f

instance Monad (State s)
 where
  return a = State (\s -> (s,a))
  c >>= f  = State (\s ->
                      let (s',a)  = unState c s
                      in unState (f a) s' 
                   )

-- Start with state 0
runZero :: State Int a -> (Int,a)
runZero f = unState f 0


-- Tick and return original value
tick :: State Int Int
tick = State (\s -> (s+1,s)) 


-- Do a sequence of computations
ticks = runZero (    tick
                 >>= const tick 
                 >>= const tick)


-----------------------------------------------------------------------------
-- Now in a type-driven fashion ---------------------------------------------
-----------------------------------------------------------------------------

-- A state monad with type-changing states
data HState s s' a = HState (s -> (s',a))
unHState (HState f) = f


-- A class for heterogeneous returns
class HReturn m x
 where
  hReturn :: a -> m x x a

instance HReturn HState s
 where
  hReturn a = HState (unState (return a))


-- A class for heterogeneous binds
class HBind m x y z
 where
  hBind :: m x y a -> (a -> m y z b) -> m x z b

instance HBind HState x y z
 where
  c `hBind` f  = HState (\s ->
                           let (s',a)  = unHState c s
                           in unHState (f a) s'
                        )


-- We use type-level naturals for different state types
data HZero   = HZero    deriving Show
data HSucc x = HSucc x  deriving Show

class HNat x 
 where
  hNat :: x -> Int

instance HNat HZero
 where
  hNat HZero = 0

instance HNat n => HNat (HSucc n) 
 where
  hNat (HSucc n) = 1 + hNat n


-- Start with state HZero
runHZero :: HState HZero n a -> (n,a)
runHZero f = unHState f HZero


-- Tick and return original value
htick :: HNat n => HState n (HSucc n) Int
htick = HState (\s -> (HSucc s,hNat s)) 


-- Do a sequence of computations
hTicks = runHZero (        htick
                   `hBind` const htick 
                   `hBind` const htick)


-- Should print: ((3,2),(HSucc (HSucc (HSucc HZero)),2))

main = print (ticks,hTicks)