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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
