Sun Aug 14 17:09:02 CEST 2011

The State Monad and State Space Models

The State Monad is  

    s -> (t, s)

What I always wondered is, shouldn't this be:

    s -> (i -> o, s)

In its basic form when t is a primitive type like Integer, an instance
of the State Monad can be used to generate a stream of values.  The
second type generates a stream if i -> o functions.

Is this enough?

I have trouble writing this down.  It seems that it's not possible to
capture the behaviour fully because the output s depends on the i
input to i->o which is one of the outputs.  So it seems that the type
needs to be a permutation of:

      i -> s -> (o, s)
      (i, s) -> (o, s)

The first one has the same type as the 2nd argument of bind.

This illustrates the point that monads are "output oriented" instead
of "input oriented"[1].

Now, the problem is the following.  When composing two state monad
functions using bind, the state is changed through all functions in
the composition.  This is *not* what we want: we want to tuple the
state: make the product of the state of the two composed entities.
I.e. the type of composition is

chainSSM :: (a -> s1 -> (b, s1)) ->
            (b -> s2 -> (c, s2)) ->
            a -> (s1,s2) -> (c, (s1,s2))

with a straightforward implemenation:

chainSSM f g = fg where
  fg a (s1,s2) = (c, (s1',s2')) where
    (b, s1') = f a s1
    (c, s2') = g b s2
In fact, the normal State monad "threading" operation is never needed.
The state is always private to the modules.  How can this kind of
composition be abstracted?  Is this an Arrow, or can it be
Applicative?  What about Category?  Haven't tried that yet..

In fact, this doesn't work: can't make composeSSM be the (.) from
Category because the type parameter that represents the state is not
constant: it grows "bigger".

The fact that the types get bigger seems to encode the property that
SSM composition cannot form loops, i.e. there is a strict order.

Is it somehow possible to automatically lift the states of the
functions such that the state is the same?  Hmm.. doesn't seem to
work.  Any other way to hide it?

Look here[2] for a "type hider", an existentially qualified type.  The
following seems to compile with -XExistentialQuantification :

data SSM i o = forall s. SSM (i -> s -> (o, s))

The thing is that you can't really do anything with these (because the
type is unknown!) until you limit it to some type class, then it's
possible to use the type class ops.

data SSM i o = forall s. SSMstate s => SSM (i -> s -> (o, s))

So, setting the limit to SSMstate which has an initState operation, it
looks that I can at least define this function:

unfoldSSM :: (SSM i o) -> [i] -> [o]
unfoldSSM (SSM tick) = f initState where
  f _ [] = []
  f s (i:is) = (o:os) where
    (o,s') = tick i s
    os = f s' is

Now the Category instance works also:

instance Category SSM where
  (.) (SSM f) (SSM g) = SSM $ g `chainSSM` f
  id  = SSM $ \i _ -> (i,())

The discrete integral then becomes:

int = SSM $ \i s -> let o = i+s in (o,o)

Define show to print the impulse response:

dirac = (1:[0,0..])
instance (Enum i, Num i, Show o) => Show (SSM i o) where
  show f = show $ take 10 $ unfoldSSM f dirac

Which prints int as:

*Main> int
*Main> int . int
*Main> int . int . int

Cool huh ;)

Now, it seems to be possible to get rid of the SSMstate altogether by
storing the initial state in the SSM object:

data SSM i o = forall s. SSM s (i -> s -> (o, s))

instance Category SSM where
  (.) (SSM f0 f) (SSM g0 g) = SSM (g0,f0) $ g `chainSSM` f
  id  = SSM () $ \i s -> (i,s)

int = SSM 0 $ \i s -> let o = i+s in (o,o)

unfoldSSM :: (SSM i o) -> [i] -> [o]
unfoldSSM (SSM init tick) = f init where
  f _ [] = []
  f s (i:is) = (o:os) where
    (o,s') = tick i s
    os = f s' is

This is even cooler.  State is now completely hidden.

Moral: initial state and update function had to be packaged together
to make it easier to hide the state type in all the other operations.

[1] http://research.microsoft.com/en-us/um/people/emeijer/publications/meijer95merging.pdf
[2] http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types