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

[Derek Elkins]

On Sun, 2009-04-19 at 20:46 -0400, Dan Doel wrote:
> 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
> 

You can build a framework around this encoding,
pack :: f a -> (forall a. f a -> r) -> r
pack x f = f x

open :: (forall r.(forall a. f a -> r) -> r) -> (forall a. f a -> r) -> r
open package k = package k

Unfortunately, pack is mostly useless without impredicativity and
lacking type lambdas requires a motley of data types to be made for f.

> '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), 

You can do this by using undefined, but without using undefined what if
F a = Void ?