ExistentialQuantifier

[Stephanie Weirich]

John Meacham wrote:
> On Wed, Feb 15, 2006 at 09:25:03AM +0000, Ross Paterson wrote:
>   
>>> when existential types are allowed in covarient positions you have
>>> 'FirstClassExistentials' meaning you can pass them around just like
>>> normal values, which is a signifigantly harder extension than either of
>>> the other two. It is also equivalent to dropping the restriction that
>>> existential types cannot 'escape' mentioned in the ghc manual on
>>> existential types.
>>>       
>> Isn't the no-escape clause fundamental to the meaning of existentials:
>> that the type is abstract after the implementation is packaged?
>>     
>
> wouldn't something that escapes end up with type exists a . a? 
> FirstClassExistentials lets you type such escaping types.
>
>   
The "escaping" mentioned in the manual is about the use of existentials:

data T = forall a. MkT  a

in the definition of

f (mkT x) = ....

the return type of f cannot mention the type variable a.   (Otherwise, a 
would escape and that
would be unsound.)

I guess you are proposing that if the type were to escape, it should be 
packaged up right again. I.e. if the definition of f were

f (mkT x) = (x,x)

then the type of f should be:

T -> exists a.(a,a)

Automatically inferring this existential seems difficult to me.  Most 
likely, one would need a type annotation on f.

f :: T -> exists a. (a,a)
f (mkT x) = (x,x)

but that is not too far from just packing the result of f into a 
different datatype existential.

data U = forall a. MkU (a,a)

f (mkU x) = MkU (x,x)

>> Of course there's always the standard encoding of existentials:
>>
>> 	exists a. T  =  forall r. (forall a. T -> r) -> r
>>
>> but in Haskell that would introduce addition liftings (boxing).
>>     
>
> Ah, that hadn't occured to me as an actual implementation tequnique.
> Interesting.
>   

Implementation issues aside, I'm not convinced that this encoding is 
that useful without some sort of impredicative polymorphism.

--Stephanie