Overlapping Instances + Existentials = Incoherent Instances
Greetings, I've actually known about this for a while, but while discussing it, it occurred to me that perhaps it's something I should report to the proper authorities, as I've never seen a discussion of it. But, I thought I'd start here rather than file a bug, since I'm not sure it isn't intended. Anyhow, here's the example: class C a where foo :: a -> String instance C a where foo _ = "universal" instance C Int where foo _ = "Int" bar :: a -> String bar x = foo x Now, normally bar generates a complaint, but if you enable IncoherentInstances, it's accepted, and it always generates "universal", even if called with an Int. Adding a 'C a' constraint to the type makes it give "Int" in the case of an Int. Now, IncoherentInstances is something most people would suggest you don't use (even people who are cool with OverlappingInstances). However, it turns out that ExistentialQuantification does the same thing, because we can write: data Ex = forall a. Ex a baz :: a -> String baz x = case Ex x of Ex x' -> foo x' and this is accepted, and always yields "universal", just like bar. So, things that you get out of an existential are allowed to make use of the general versions of overlapping instances if any fit. So, I never really regarded this as anything more than an oddity that's unlikely to come up. And it might be working as intended. But I thought perhaps I should ask: is this intended? One could probably build a case that baz should only be accepted if IncoherentInstances are enabled, since it's doing about the same thing. I'm not really sure how far back this behavior goes. I've probably known about it for several 6.X releases without mentioning it except as a fun party fact (apologies). Is this the way things are supposed to work? (And sorry if I just missed the discussion somewhere. I searched the trac and didn't see anything very promising.) Cheers, -- Dan
Dan,
class C a where foo :: a -> String
instance C a where foo _ = "universal"
instance C Int where foo _ = "Int"
[...]
Now, IncoherentInstances is something most people would suggest you don't use (even people who are cool with OverlappingInstances). However, it turns out that ExistentialQuantification does the same thing, because we can write:
data Ex = forall a. Ex a
baz :: a -> String baz x = case Ex x of Ex x' -> foo x'
and this is accepted, and always yields "universal", just like bar. So, things that you get out of an existential are allowed to make use of the general versions of overlapping instances if any fit.
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. Cheers, Stefan
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
This is a tricky one. The motivating example is this: -- Overlapping instances instance Show a => Show [a] where ... instance Show Char where ... data T where MkT :: Show a => [a] -> T f :: T -> String f (MkT xs) = show xs ++ "\n" Here it's clear that the only way to discharge the (Show [a]) constraint on 'x' is with the (Show a) dictionary stored inside the MkT. Yet doing so means ignoring the possibility that a=Char. So, for example, if we go h = case MkT "boo" of MkT xs -> show xs ++ "\n" we'll get the output string "['b','o','o']", not "boo". So yes, that's incoherent, in the sense that if we did the case-elimination we'd get (show "boo" ++ "\n"), and that would give a different result. Why does GHC have this behaviour? Because in the case of type signature, such as g :: [a] -> String g xs = show xs ++ "\n" we can change g's type signature to make it compile without having to choose which instance to use: g :: Show [a] => [a] -> String But with an existential type there is no way we can alter 'f' to make it work; it's the definition of T that would have to change. So I can't say it's perfect, but it seems too much of a Big Hammer to say IncoherentInstances for f. Anyway, that's the rationale. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Dan Doel | Sent: 03 February 2010 03:08 | To: glasgow-haskell-users@haskell.org | Subject: Overlapping Instances + Existentials = Incoherent Instances | | Greetings, | | I've actually known about this for a while, but while discussing it, it | occurred to me that perhaps it's something I should report to the proper | authorities, as I've never seen a discussion of it. But, I thought I'd start | here rather than file a bug, since I'm not sure it isn't intended. Anyhow, | here's the example: | | class C a where | foo :: a -> String | | instance C a where | foo _ = "universal" | | instance C Int where | foo _ = "Int" | | bar :: a -> String | bar x = foo x | | Now, normally bar generates a complaint, but if you enable | IncoherentInstances, it's accepted, and it always generates "universal", even | if called with an Int. Adding a 'C a' constraint to the type makes it give | "Int" in the case of an Int. | | Now, IncoherentInstances is something most people would suggest you don't use | (even people who are cool with OverlappingInstances). However, it turns out | that ExistentialQuantification does the same thing, because we can write: | | data Ex = forall a. Ex a | | baz :: a -> String | baz x = case Ex x of | Ex x' -> foo x' | | and this is accepted, and always yields "universal", just like bar. So, things | that you get out of an existential are allowed to make use of the general | versions of overlapping instances if any fit. | | So, I never really regarded this as anything more than an oddity that's | unlikely to come up. And it might be working as intended. But I thought | perhaps I should ask: is this intended? One could probably build a case that | baz should only be accepted if IncoherentInstances are enabled, since it's | doing about the same thing. | | I'm not really sure how far back this behavior goes. I've probably known about | it for several 6.X releases without mentioning it except as a fun party fact | (apologies). Is this the way things are supposed to work? (And sorry if I just | missed the discussion somewhere. I searched the trac and didn't see anything | very promising.) | | Cheers, | -- Dan | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
participants (3)
-
Dan Doel -
Simon Peyton-Jones -
Stefan Holdermans