[<<][compsci][>>][..]
Thu Aug 18 00:10:54 CEST 2011

## Existential types

I was trying to understand why pattern matching followed by
application works fine, but pattern matching and returning doesn't
work.  In other words: why don't existentials support record
selectors, and why is passing them as arguments to functions not an
issue?

A typical example: a type with a hidden value type and a function with
hidden input type.  Both are the same so the value can be passed to
the function.

data Exst a = forall b. Exst b (b->a)

The following doesn't type check, for the simple reason that it is
completely unknown what type the function produces.  It can be
anything.

value (Exst v f) = f

It's not that the pattern matching itself doesn't work.  The following
works fine:

eval1 :: Exst a -> a
eval1 (Exst v f) = f v

The reason is that we don't know the type of v and f, only how they
are related: we do know that if we apply f to v we get the type that
the Exst is parameterized by.

It is also possible to pass the value to a function that expects a
parametric type that is the same as the one that's specified:

eval2 :: b -> (b -> a) -> a
eval2 v f = f v

eval3 (Exst v f) = eval2 v f

* * *

Now for the real problem I'm facing, given a data type that represents
a Kleisli arrow

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

Construct the type isomorphism:

iso :: (i -> Kl () o) -> Kl i o
iso = undefined

No matter what I try.  Case statements or CPS, I still can't get the
types to match: it always sees the type variable in the data
declaration as different from the one in any other specification.

Wait, I think I finally get it.  There is simply no way of knowing
that the s that is passed to kl is the same as the s of kl.

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

It's possible to write that line with an implicit s, but the point is
still the same: the type that was fixed when the Kl that's being
unpacked was created could be completely different from the new
instance we're creating here.  The information on what that type was
is no longer present in the type of f.

iso f = Kl \$ \i -> (\(Kl kl) -> kl ()) (f i)

In a Monad, the join operation flattens two layers of wrapping into
one.  Doing this with an existentially qualified type doesn't work if
this data needs to be combined in any way, because all information
that they might be of compatible types has been deleted.

The same goes for bind: it takes information from outside the monad
and inserts it inside, crossing a border where type information has
been deleted.

What does work is to unpack, combine, repack.  Stuff that comes out of
a single wrapper can all be combined together.