[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)

[Luke Palmer]

On Tue, Jan 20, 2009 at 1:14 PM, David Menendez <dave at zednenem.com> wrote:

> On Tue, Jan 20, 2009 at 2:51 PM, Mauricio <briqueabraque at yahoo.com> wrote:
> >>> But how is this:
> >>> data SomeNum = forall a. SN a
> >>> different from:
> >>> data SomeNum = SN (forall a. a)
> >
> >> At a glance they look the same to me — but only the first is accepted by
> >> ghc.
> >
> > Following the link you pointed in the last
> > message, I found this at 8.8.4.1:
> >
> > data T a = T1 (forall b. b -> b -> b) a
>

The constructor here is irrelevant.  The function here can do anything a
top-level function of type:

something :: b -> b -> b

I like to think about quantification in this regard in terms of
isomorphisms.  Think about what a function of type forall b. b -> b -> b can
do.  It cannot do anything with its arguments, because it must work on all
types, so it only has one choice to make: it can return the first argument,
or it can return the second argument.

So, forall b. b -> b -> b  is isomorphic to Bool.

For symmetry, the constructor T1 has type:

T1 :: (forall b. b -> b -> b) -> a -> T1 a


>
>
> > If I understand properly, it can be activated
> > with -XPolymorphicComponents. It's different
> > from my example, but I would like to know what
> > it does that this can't:
> >
>
> data T a = forall b. T1 (b->b->b) a
>

The constructor T1 here has type:

T1 :: forall b. (b -> b -> b) -> a -> T1 a

See the difference?

You can pass the latter a function of any type you choose, eg. (Int -> Int
-> Int) or ((Bool -> Bool) -> (Bool -> Bool) -> (Bool -> Bool)).  So when
somebody gets a T from you, they have no idea what type the function you
gave it was, so they can only use it in limited ways (in this case, nothing
useful at all can be done with it).

Here's another existential type:

data T' a = forall b. T' (b -> a) b

Here, a T' contains a value of some type b -- who knows what it is -- and a
function to get from that value to an a.  Since we don't know anything about
b, all we can do is to apply the function.

T' a is isomorphic to a.  But it might have different operational behavior;
e.g. maybe a is a huge list which is cheaply generated from some small
generator value (of type b).  Then if you pass a T' around, it's the same as
passing that big list around, except for you don't cache the results of the
list, improving memory performance.  It's like inverse memoization.

Not all existential types are for inverse memoization, this is just one
case.

I found it easiest to reason about these with the types of the constructors,
and thinking about what non-quantified type they are isomorphic to.

Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090120/782127fd/attachment.htm