On Wednesday 03 February 2010 11:34:27 am Stefan Holdermans wrote: > I don't think it's the same thing. The whole point of the existential > is that at the creation site of any value of type Ex the type of the > value being packaged is hidden. At the use site, therefore, the only > suitable instance is the one for C a. In particular, there is no way > for the baz to tell whether an Int is wrapped in the existential. > > However, if we pack a dictionary along, as in > > data Ex = forall a. C a => Ex a > > then, you'll find that baz will pick the dictionary supplied with the > existential package rather than the one from the general instance.
This is (I think) exactly the behavior that IncoherentInstances enables, though, except for universal quantification. If our function has the type: forall a. a -> String then the only instance that can be picked for the parameter is the C a instance, because the function knows nothing about a; a is hidden from the function's perspective, rather from a global perspective, but the function is the one picking the instance to use, since it isn't given one. If instead we pass the dictionary explicitly: forall a. C a => a -> String the function uses that dictionary. In fact, if existentials were first class, we could directly write some isomorphic types that show the analogy: forall a. a -> String ~= (exists a. a) -> String forall a. C a => a -> String ~= (exists a. C a => a) -> String The bottom two naturally work, because we're passing the dictionary. On the top, the existential version works, but the universal version doesn't, unless we enable an extra extension. As a final data point, one can encode existential types via their universal eliminators: type Ex' = forall r. (forall a. a -> r) -> r hide :: forall a. a -> Ex' hide x k = k x open :: (forall a. a -> r) -> Ex' -> r open f ex = ex f Now we can try to write the unconstrained function: quux :: a -> String quux x = open foo (hide x) But, this gives an error telling us that we need IncoherentInstances. -- Dan _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users