[Haskell-cafe] Fundeps and overlapping instances

[Iavor Diatchki]

Hello,

On Wed, Jul 7, 2010 at 2:14 PM, Simon Peyton-Jones <simonpj at 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****
>
>   bad = g . f****
>
> ** **
>
> 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****
>
>   bad = g . f****
>
> **
>

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120530/a539a3ae/attachment.htm>