Is it time to start deprecating FunDeps?
anthony_clayden at clear.net.nz
Wed May 1 11:06:26 CEST 2013
> AntC <anthony_clayden at ...> 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
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.)
More information about the Haskell-prime