TypeFamilies vs. FunctionalDependencies & type-level recursion

[Iavor Diatchki]

Hello,

On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

> | >    class C a b | a -> b where
> | >      foo :: a -> b
> | >      foo = error "Yo dawg."
> | >
> | >    instance C a b where
> |
> | The instance 'C a b' blatantly violates functional dependency and
> | should not have been accepted. The fact that it was is a known bug in
> | GHC. The bug keeps getting mentioned on Haskell mailing lists
> | about every year. Alas, it is still not fixed. Here is one of the
> | earlier messages about it:
> |
> |   http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html
>
> Wait.  What about
>        instance C [a] [b]
> ?  Should that be accepted?  The Coverage Condition says "no", and indeed
> it is rejected. But if you add -XUndecidableInstances it is accepted.
>
> It's just the same for
>        instance C a b
> It is rejected, with the same message, unless you add
> -XUndecidableInstances.
>
> Do you think the two are different?  Do you argue for unconditional
> rejection of everything not satisfying the Coverage Condition, regardless of
> flags?
>
>
No, those two are not different, the instance "C [a] [b]" should also be
rejected because it violates the functional dependency.  The fact
that -XUndecidableInstances accepts this is exactly the bug that keeps being
mentioned on the lists every now and then.  The reason that this instance
violates the functional dependency is that it allows us to conclude both "C
[Int] [Bool]", and "C [Int] [Char]", and clearly "[Int] = [Int]", but
"[Bool] /= [Char]".

The general rule defining an FD on a class like "C" is the following logical
statement:
"forall a b1 b2.  (C a b1, C a b2) => (b1 = b2)"

(So I think that the basic concept is really very simple and precise.  I
agree that the implementation can be tricky, but a lot of the difficulties
are shared with type families---we are just dealing with a hard problem.)

With simple instances (no contexts) it is easy to check if a set of
instances is consistent with the FDs of the classes, however when we have
conditional instance the task is harder.  This is why we have approximations
that ensure consistency (e.g., the Coverage Condition).  My understanding is
that the coverage condition in GHC ensures both consistency with the FDs,
and termination of the process.  In the past we had another condition,
 which ensured consistency but not necessarily termination (I forget its
name now but, basically, the rule said that all variables in the target of
an FD should be determined from the variables in the source of the FD, but
we can use FDs in the context of the instance).   I think the GHC bug is
that with -XUndecidableInstances, instances are not validated at all wrt to
FDs.  A way to fix that would be to switch to using the old FD validation
rule when -XUndecidableInstances are turned on.

-Iavor


Simon
>
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-prime/attachments/20110615/ce99354f/attachment-0001.htm>