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