ExistentialQuantifier
Stephanie Weirich
sweirich at cis.upenn.edu
Wed Feb 15 10:47:29 EST 2006
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
More information about the Haskell-prime
mailing list