Ralf Laemmel Ralf.Laemmel at cwi.nl
Fri Jul 2 10:15:15 EDT 2004

```
-------------- 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 ----------------------------------
-----------------------------------------------------------------------------

data State s a = State (s -> (s,a))
unState (State f) = f

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

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

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)

```