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

[Dan Doel]

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. 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. These two are (roughly?) isomorphic, 
because you can pass the function:

  f :: forall a. F a -> (exists a. F a)
  f x = x

to the eliminator and get back a value with the existential type.

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). And you can also make a 
type:

  data E f y = forall a. E (f a -> y)

where E F Y is the same as (exists a. F a -> Y). But here you'd find that you 
can write:

  from :: (E f y) -> ((forall a. f a) -> y)
  from (E f) fa = f fa

but not:

  to :: ((forall a. f a) -> y) -> (E f y)
  to f = E (\fa -> f fa)

so these two are not equivalent, either. Rather:

  exists a. (F a -> Y) ~ forall r. (forall a. (f a -> y) -> r) -> r

where we have:

  from :: E f y -> (forall r. (forall a. (f a -> y) -> r) -> r)
  from (E f) k = k f

  to :: (forall r. (forall a. (f a -> y) -> r) -> r) -> E f y
  to k = k E

Similarly, you can encode universals as higher-rank existential eliminators. 
Of course, there are some cases where things reduce more nicely, like:

  (exists a. F a) -> Y ==> forall a. (F a -> Y)

In any case, despite being able to encode existentials in this way, or use 
existentially quantified data types, it might be nice to have first-class 
existential types like UHC. But, I seem to recall this being investigated for 
GHC in the past, and it was decided that it added too much complexity with the 
rest of GHC's type system. My information is sketchy and third hand, though, 
and perhaps things have changed since then.

-- Dan