[Haskell-cafe] Existential quantification problem

[Dan Doel]

On Thursday 10 July 2008, Marco Túlio Gontijo e Silva wrote:
> Hello,
>
> how do I unbox a existential quantificated data type?
>
> > {-# LANGUAGE ExistentialQuantification #-}
> > data L a = forall l. L (l a)
> > unboxL (L l) = l
>
> is giving me, in GHC:
>
>     Inferred type is less polymorphic than expected
>       Quantified type variable `l' escapes
>     When checking an existential match that binds
>         l :: l t
>     The pattern(s) have type(s): L t
>     The body has type: l t
>     In the definition of `unboxL': unboxL (L l) = l

You don't. Or, at least, you don't do it that way. The point of an existential 
is that the quantified type is 'forgotten', and there's no way to get it 
back. That's good for abstraction, in that it restricts you to using some 
provided interface that's guaranteed to work with the forgotten type, but it 
means that you can't just take things out of the existential box.  Instead, 
you have to use them in ways that make the forgotten type irrelevant (that 
is, ways that are parametric in the corresponding type).

The type of the unboxL function in a type system with first-class existentials 
is something like:

    unboxL :: L a -> (exists l. l a)

Of course, GHC doesn't do first-class existentials, otherwise you'd probably 
not be bothering with the datatype in the first place. :)

The proper way to eliminate an existential is (as mentioned above) with a 
universal:

    elim :: (exists l. l a) -> (forall l. l a -> r) -> r
    elim e f = f e

Or, since existentials in GHC are restricted to data types:

    elim :: L a -> (forall l. l a -> r) -> r
    elim (L e) f = f e

Of course, as has already been noted,

    elim foo (\l -> stuff)

is equivalent to:

    case foo of
      L l -> stuff

and doesn't need rank-2 polymorphism enabled, to boot. :)

-- Dan