Overlapping Instances + Existentials = Incoherent Instances
Dan Doel
dan.doel at gmail.com
Wed Feb 3 12:11:36 EST 2010
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
More information about the Glasgow-haskell-users
mailing list