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

[Dan Doel]

On Sunday 19 April 2009 7:11:51 pm wren ng thornton wrote:
> 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.

No, I'm relatively sure this doesn't work. Take, for instance, F a = a for 
simplicity. Then we can say:

  i :: Int
  i = 5

  ei :: exists a. a
  ei = i

Because ei's type, exists a. a, means "this expression has some unknown type." 
And certainly, the value i does have some type; it's Int.

By contrast, you won't be writing:

  ei' :: forall a. a
  ei' = i

and similarly:

  ei'' :: forall a. () -> a
  ei'' () = i

is not a correct type, because i is not a value that belongs to every type. 
However, we can write:

  ei''' :: forall r. (forall a. a -> r) -> r
  ei''' k = k i

as well as translations between types like it and the existential:

  toE :: (forall r. (forall a. a -> r) -> r) -> (exists a. a)
  toE f = f (\x -> x)

  toU :: (exists a. a) -> (forall r. (forall a. a -> r) -> r)
  toU e k = k e

'forall' in GHC means universal quantification. It's doesn't work as both 
universal and existential quantification. The only way it's involved with 
existential quantification is when you're defining an existential datatype, 
where:

  data T = forall a. C ...

is used because the type of the constructor:

  C :: forall a. ... -> T

is equivalent to the:

  C :: (exists a. ...) -> T

you'd get if the syntax were instead:

  data T = C (exists a. ...)

Which is somewhat confusing, but forall is standing for universal 
quantification even here.

> 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.

I don't really understand what you mean by "type lifting". But although you 
might be able to write functions with types similar to what you've listed 
above (for instance, of course you can write a function:

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

simply because this is essentially a function with type

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

and you can do that by instantiating the argument to any type, and then hiding 
it in an existential), this does not mean the types above are isomorphic, 
which they aren't in general.

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

Well, you can get rid of the extra bottom with

  data E f = forall a. E !(f a)

but first-class existentials are still desirable because introducing a new 
type for every existential is annoying. It's comparable to having to write a 
new class for every combination of argument and result types to mimic first 
class functions in Java (aside from first class functions being more 
ubiquitous in their usefulness, although perhaps it only appears that way 
because we don't have easy use of existential types).

-- Dan