On Wed, Jul 7, 2010 at 2:14 PM, Simon Peyton-Jones
<simonpj@microsoft.com> wrote:
We can’t permit overlap for type families because it is unsound
to do so (ie you can break “well typed programs don’t go wrong”).
But if it’s unsound for type families, it would not be surprising if it
was unsound for fundeps too. (I don’t think anyone has done a
soundness proof for fundeps + local constraints + overlapping instances, have
they?) And indeed I think it is.
It would be unsound only if the functional dependencies are not checked properly (which, as you say, is similar to the check for type families). Here is an example of a sound overlap:
class C a b | a -> b
instance C String Char
instance C [a] a
Indeed, it would be OK to allow this sort of overlap for type families too, although there it would not be useful, because the more general case already provides the same information as the more specific one. In the case of overlapping instances, the more specific instance might provide a different implementation for the class methods, as usual. (disclaimer: I'm not a fan of overlapping instances----I think that some of the alternative proposals, such as the instance chains work, are nicer, but one would have to do same sort of checks there too).
Imagine a system “FDL” that has functional dependencies
and local type constraints. The big deal about this is that you get to exploit
type equalities in *given* constraints. Consider Oleg’s
example, cut down a bit:
class C a b | a -> b
instance C Int Bool
newtype N2 a = N2 (forall b.
C a b => b)
t2 :: N2 Int
t2 = N2 True
We end up type-checking (True :: forall b. C Int b =>
b). From the functional dependency we know that (b~Bool), so the
function should typecheck. GHC rejects this program; FDL would not.
But making use of these extra equalities in “given”
constraints is quite tricky. To see why look first at Example 1:
module X where
class C a b | a -> b
data T a where
MkT :: C a b => b -> T a
module M1 where
import X
instance C Int Char where ...
f :: Char -> T Int
f c = MkT c
module M2 where
import X
instance C Int Bool
g :: T Int -> Bool
g (MkT x) = x
module Bad where
import M1
import M2
bad :: Char -> Bool
This program is unsound: it lets you cast an Int to a Bool;
result is a seg-fault.
You may say that the problem is the inconsistent functional
dependencies in M1 and M2. But GHC won’t spot that. For type
families, to avoid this we “eagerly” check for conflicts in
type-family instances. In this case the conflict would be reported when
compiling module Bad, because that is the first time when both instances are
visible together.
So any FDL system should also make this eager check for
conflicts.
I completely agree with this---we should never allow inconsistent instances to exist in the same scope.
What about overlap? Here’s Example 2:
{-# LANGUAGE IncoherentInstances #-}
module Bad where
import X
-- Overlapping instances
instance C Int Bool --
Instance 1
instance C a [a] --
Instance 2
f :: Char -> T Int
f c = MkT c --
Uses Instance 1
g :: T a -> a
g (MkT x) = x --
Uses Instance 2
bad :: Char -> Int
As in the above example, this program violates the functional dependency on class C and should be rejected, because the two instances are not consistent with each other.
But at the moment GHC makes an exception for *existentials*.
Consider Example 3:
class C a b | a -> b
-- Overlapping instances
instance C Int Bool --
Instance 1
instance C a [a] --
Instance 2
data T where
MkT :: C a b => a -> b -> T
f :: Bool -> T
f x = MkT (3::Int) x --
Uses Instance 1
g :: T -> T
g (MkT n x) = MkT n
(reverse x) -- Uses Instance 2
bad :: Bool -> T
bad = g . f
This program is malformed for the same reason as the previous one: the two instances violate the functional dependency on the class.
But even nuking
IncoherentInstances altogether is not enough. Consider this variant of
Example 3, call it Example 4:
module M where
class C a b | a -> b
instance C a [a] --
Instance 2
data T where
MkT :: C a b => a -> b -> T
g :: T -> T
g (MkT n x) = MkT n (reverse x) -- Uses Instance
2
module Bad where
import M
instance C Int Bool --
Instance 1
f :: Bool -> T
f x = MkT (3::Int) x --
Uses Instance 1
bad :: Bool -> T
bad = g . f
We must be thinking about these examples in a rather different way :-) Like the others, I'd say that this program should be rejected because it violates the functional dependency on the class and should be rejected.
The way I think of a functional dependency on a class is that it restricts what instances are allowed to co-exist in the same scope. So GHC needs to ensure that its instance database never contains instances that violate the functional dependency property. This amounts to three checks:
1. Check that an instance is consistent with itself. For example, this should be rejected:
instance C a b
because it allows C Int Bool and C Int Char which violate the functional dependency.
2. Check that an instance is consistent with all other instances in scope. Note that this is orthogonal to the overlapping check: instances need to be consistent with the fun. dep. independent of overlap.
3. Check that instances imported from different modules are consistent with each other. This is really a special case of 2, and GHC must already be doing some checking at this point to avoid duplicated instances.
It is important that the checks for consistency are sound. They are not likely to be complete (i.e., we might reject some programs that do not really violate the fun.dep. but GHC can't see it),
but that's OK. The usual rule, I forget its name, falls in this category.
Finally for the payoff of all this: because we know that GHC is going to enforce the fun. dep. invariant, we can use it when we type check things. For example, consider the standard example:
f :: (C a b, C a c) => a -> b -> c
f x y = y
This is OK, but only as long as GHC ensures that all instances of C satisfy the fun. dep. invariant. If the invariant is satisfied, however, then we know that whenever "f" is used, the instances that will be used to discharge its constraints are going the satisfy the fun. dep. and so "b" and "c" will be the same.
-Iavor