Sat Aug 20 22:14:28 CEST 2011

Existential Monad problem: solved!

One last attempt at trying to understand why this can't work:

  (.>) v f = f v  -- Patern binding doesn't work with existentials.

  type Kl i o = i -> Kl1 o
  data Kl1 o = forall s. Kl1 (s -> (s,o))

  bind :: (Kl1 i) -> (i -> Kl1 o) -> (Kl1 o)
  bind mi f =
    Kl1 $ \(s1,s2) ->
          mi      .> (\(Kl1 u1) -> (u1 s1) .> (\(s1', i)  ->
          (f i)   .> (\(Kl1 u2) -> (u2 s2) .> (\(s2', o)  ->

The problem here is that the s1,s2 we feed into the unpacked Kl1 are
not compatible.  The type of u1 and u2 is completely unknown in the
expression of bind.

To understand this, let's try to take a look at Ryan's answer[1].
Paraphrased, look at what happens if we have an f doing something

  f i :: Bool -> Kl1 o
  f i = if i then kl1 else kl2

where kl1 and kl2 could have different state types.  Because the above
is possible, you really can't assume anything.

The problem is really that the dependence on the i input is "too
powerful".  In the arrow approach for the type

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

it seems to work because everything is neatly tucked in; no state
change possible.

[1] http://www.mail-archive.com/haskell-cafe@haskell.org/msg92609.html