[Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first
release
Dan Doel
dan.doel at gmail.com
Sun Apr 19 22:04:44 EDT 2009
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
More information about the Haskell-Cafe
mailing list