[<<][meta][>>][..]
Thu Aug 18 17:48:23 CEST 2011

Writing down the Kleisli isomorphism with existential types.

Oleg's reply to [1]: It is possible to do this by moving the
quantification inside:

  type Kl i o = i -> Kl1 o
  data Kl1 o = forall s. Kl1 (s -> (s,o))
  iso :: (i -> Kl () o) -> Kl i o
  iso f = \i -> f i ()

Adding a data wrapper and an unpack function written as a pattern
match as before (to avoid other GHC issues) gives:

  data Kl i o = Kl (i -> Kl1 o)
  data Kl1 o = forall s. Kl1 (s -> (s,o))
  iso :: (i -> Kl () o) -> Kl i o
  iso f = Kl $ \i -> (\(Kl kl) -> kl ()) (f i) 

And lo and behold, the extra initial state parameter can just be
added!

  data Kl i o = Kl (i -> M o)
  data M o = forall s. M s (s -> (s,o))
  iso :: (i -> Kl () o) -> Kl i o
  iso f = Kl $ \i -> (\(Kl kl) -> kl ()) (f i) 

I wonder if now it will break at another point.  Maybe it's no longer
possible to write composition of Kl?

Let's give it a try.  But first, let's try bind again since the monad
is naked anyway.  Hmm.. can't do it just like that.

I was thinking though, since we're not chaining states, just inputs
and outputs, that it might be possible to pull it off anyway: all
states are self-contained.

So, trying to write compose for signature (i -> (s, s -> (s,o))).
This seems to get stuck because the initial state is hidden behind the
input, so it can't be bubbled up.

In other words, the following isomorphism doesn't seem to exist:

  (i -> (s, s -> (s, o)))  ->  (s, i -> s -> (s, o))
  
Or does it?  What if we make i part of a class that has somehow a
"default" value.  Because we do know that once unpacked, the value we
find does not depend on i.

What I wonder is why these tricks are necessary.  The idea does seem
to be sound though.  Let's try it out.

Ok, I found a trick to unlock the initial state and write a
composition function:


  class Unlock a where
    key :: a

  compose :: (Unlock a, Unlock b) =>
             (a -> (s1, (s1 -> (s1, b)))) ->
             (b -> (s2, (s2 -> (s2, c)))) ->
             (a -> ((s1,s2), ((s1,s2) -> ((s1,s2), c))))
    
  compose f1 f2 = f12 where 
    (i1, _) = f1 key {- u -}
    (i2, _) = f2 key {- u -}
    f12 a = ((i1,i2), u12) where
      u12 (s1, s2) = ((s1', s2'), c) {- p -} where
        (_, u1)  = f1 a  {- u -}
        (s1', b) = u1 s1 
        (_, u2)  = f2 b  {- u -}
        (s2', c) = u2 s2 

Can this be used to implement compose for the wrapped type?  There are
4 unpacks that cross the hiding barrier, and one repack.  Let's
convert to CPS:

  (.>) v f = f v

  compose' :: (Unlock a, Unlock b) =>
              (a -> M b) ->
              (b -> M c) ->
              (a -> M c)

  compose' f1 f2 = 
    (f1 key) .> (\(M (i1, _)) ->
    (f2 key) .> (\(M (i2, _)) ->
    \a -> M $ ((i1, i2),
               (\(s1, s2) ->
                 (f1 a)  .> (\(M (_, u1)) ->
                 (u1 s1) .> (\(s1', b)    ->
                 (f2 b)  .> (\(M (_, u2)) ->
                 (u2 s2) .> (\(s2', c)    ->
                 ((s1',s2'), c)
                 ))))))))

It looks like it's really either/or.  If you put the quantification as
Oleg suggested, it doesn't seem possible to write the compose
function.  If you put it like I had it originally, you can't write the
isomorphism.

Stuck again.  Going in circles.

Reply :
 - real point is extra s
 - to get the s behind the i, use a constant argument
 - write compose in his example nomenclature
 - the contrived syntax to avoid pattern binding errors.


EDIT: the "key" problem already indicates that something isn't right:
there is a depedency in the types that I simply ignore here..

[1] http://www.haskell.org/pipermail/haskell-cafe/2011-August/094718.html




[Reply][About]
[<<][meta][>>][..]