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

[Dan Doel]

On Sunday 19 April 2009 9:31:27 pm Derek Elkins wrote:
> > 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 ?

If it is, then you're giving me a Void, and I'm putting it in a box. 
Apparently I've not installed Agda since I installed GHC 6.10.2, but I'd 
expect something like the following to work:

  data VoidF (t : Set) : Set where

  data Unit : Set where
    unit : Unit

  data ∃ (f : Set -> Set) : Set1 where
    box : {t : Set} -> f t -> ∃ f

  box-it : (forall t -> VoidF t) -> ∃ VoidF
  box-it void = box (void Unit)

It's just going to be difficult to get a value with type forall t -> VoidF t 
in the first place.

-- Dan