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

## Writing down the Kleisli isomorphism with existential types.

```Oleg's reply to : 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

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.

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

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