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.
Implementation issues aside, I'm not convinced that this encoding is
that useful without some sort of impredicative polymorphism.
More information about the Haskell-prime