> AntC <anthony_clayden@...> writes:
>
> > <oleg <at> ...> 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.)
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
