Re: Is it time to start deprecating FunDeps?

1 May 2013

      ...
AntC  writes:
...
 writes:
I think this mechanical way is not complete.
On further thought/experiment, I rather think it is -- for one of your 
counter examples.

Firstly, I apologise to Oleg. I had mis-remembered his solution to the 
class Sum example ...
...
...
class Sum x y z | x y -> z, x z -> y
your own solution has a bunch of helper classes (each with one-
directional FunDeps).
This Sum is actually a helper called Sum2 in the PeanoArithm module. 
Here's Oleg's full code (modulo alpha renaming):
{-
    class Sum2 a b c | a b -> c, a c -> b
    instance Sum2 Z b b
    instance (Sum2 a' b c') => Sum2 (S a') b (S c')

    -- note that in the FunDeps, var a is not a target
    -- so the instances discriminate on var a
-}

And I must apologise to myself for doubting the mechanical translation in 
face of cyclical FunDeps. Here it is:

    class Sum2 a b c         -- | a b -> c, a c -> b
    instance (b ~ c) => Sum2 Z b c
    instance (c ~ (S c'), Sum2 a' b c') => Sum2 (S a') b c
...
Your [Oleg's] solution has a single instance declared for the 
Sum class, with three bare typevars. So it is valid by step 1. of the 
rules I gave. (In your solution all the 'hard work' is done by the 
helpers, which are constraints on that single instance.)
That much I had remembered correctly. So I don't need to change the Sum 
class (except to remove the FunDep):

    class Sum a b c          -- | a b -> c, a c -> b, b c -> a
    instance (Sum2 a b c, Sum2 b a c) => Sum a b c

The tests from Oleg's code (ta1, ta2) infer the same types. Test ta3 fails 
to compile -- as it does for Oleg.

(My code does need UndecidableInstances, as does Oleg's.)