[Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release

[wren ng thornton]

Dan Doel wrote:
> On Sunday 19 April 2009 4:56:29 pm wren ng thornton wrote:
> > Bulat Ziganshin wrote:
> > > Hello R.A.,
> > >
> > > Sunday, April 19, 2009, 11:46:53 PM, you wrote:
> > > > Does anybody know if there are any plans to incorporate some of
> > > > these extensions into GHC - specifically the existential typing ?
> > >
> > > it is already here, but you should use "forall" keyword instead odf
> > > "exists"
> >
> > More particularly, enable Rank2Types and then for any type lambda F and
> > for any type Y which does not capture @a@:
> >
> > (x :: exists a. F a) ==> (x :: forall a. F a)
> >
> > (f :: exists a. (F a -> Y)) ==> (f :: (forall a. F a) -> Y)
>
> Eh? I don't think this is right, at least not precisely. The first is 
> certainly not correct, because
> 
>   exists a. F a
> 
> is F A for some hidden A, whereas
> 
>   forall a. F a
> 
> can be instantiated to any concrete F A.

Yes, however, because consumers (e.g. @f@) demand that their arguments 
remain polymorphic, anything which reduces the polymorphism of @a@ in 
@x@ will make it ineligible for being passed to consumers. Maybe not 
precise, but it works.

Another take is to use (x :: forall a. () -> F a) and then once you pass 
() in then the return value is "for some @a@". It's easy to see that 
this is the same as the version above.


> A higher rank encoding of this 
> existential would be:
> 
>   forall r. (forall a. F a -> r) -> r
> 
> encoding the existential as its universal eliminator, similar to encoding an 
> inductive type by its corresponding fold.

Exactly. Whether you pass a polymorphic function to an eliminator (as I 
had), or pass the universal eliminator to an applicator (as you're 
suggesting) isn't really important, it's just type lifting:

(x :: forall a. F a) ==> (x :: forall r. (forall a. F a -> r) -> r)

(f :: (forall a. F a) -> Y) ==> (f :: ((forall a. F a -> Y) -> Y) -> Y))


The type lifted version is more precise in the sense that it 
distinguishes polymorphic values from existential values (rather than 
overloading the sense of polymorphism), but I don't think it's more 
correct in any deep way.


> What you can do in GHC is create existentially quantified data types, like so:
> 
>   data E f = forall a. E (f a)
> 
> Then E F is roughly equivalent to (exists a. F a).

But only roughly. E F has extra bottoms which distinguish it from 
(exists a. F a), which can be of real interest.

-- 
Live well,
~wren