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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe