writes:

I think this mechanical way is not complete.

Thanks Oleg for the counter-examples. I find them both rather mischievous, because they both go beyond the limits of what FunDeps can do: In your 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). Your 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.) (But I do concede that in general the translation rules I gave do not work for cyclic dependencies. I'm looking into whether I can beef up the rules to at least validate against a FunDeps class for instances that use EqC's.) In your overlap example you introduce a definition that won't compile!

{- -- correctly prohibited! instance x ~ Bool => C1 [Char] x where foo = const True -}

You expect too much if you think a mechanical translation will 'magic' a non-compiling program into something that will compile. I do expect equality constraints to not play well with overlaps. Combining FunDeps with overlaps is also hazardous. I'm only claiming that EC's will be at least as good. In the HDeleteMany example I gave in the OP, yes the translation did solve a problem that blocked compiling. (And the HList paper also gives a solution using FunDep's which needs helper classes.) I'm not claiming that will always work. I'm not claiming that equality constraints are uniformly better than FunDeps; I'm only claiming that they're at least equivalent in power, and sometimes give easier to understand code. And I find FunDeps not very, err, functional.

(1) There's a mechanical way to translate FD programs with non-overlapping instances to TF (and of course vice versa). For example, let's reconsider Oleg's example.

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-}

class Sum x y z | x y -> z, x z -> y instance Sum Int Float Double

class (SumF1 x y ~ z, SumF2 x z ~ y) => SumF x y z type family SumF1 x y type family SumF2 x z instance SumF Int Float Double type instance SumF1 Int Float = Double type instance SumF2 Int Double = Float

As we know, GHC's intermediate language only records TF type improvement but not FD type improvement. Therefore,

f :: SumF Int Float z => z -> z f _ = (1.0 :: Double)

{- fails to type check f2 :: Sum Int Float z => z -> z f2 _ = (1.0 :: Double) -}

(2) There's an issue in case of overlapping instances as pointed out by Oleg. The source of the issue is that overlapping type class instances are treated differently compared to overlapping type family instances. In principle, both formalisms (FD and TF) are equivalent in expressive power. (3) As Edward points out, there are many good reasons why we want to keep FDs. Just compare the above FD program against its TF equivalent! I enjoy using both formalisms and would be unhappy if we'd get rid of one of them :) -Martin On Tue, Apr 30, 2013 at 9:18 AM, wrote:

Anthony Clayden wrote:

...

Better still, given that there is a mechanical way to convert FunDeps to equalities, we could start treating the FunDep on a class declaration as documentation, and validate that the instances observe the mechanical translation.

I think this mechanical way is not complete. First of all, how do you mechanically convert something like

class Sum x y z | x y -> z, x z -> y

Second, in the presence of overlapping, the translation gives different results: compare the inferred types for t11 and t21. There is no type improvement in t21. (The code also exhibits the coherence problem for overlapping instances: the inferred type of t2 changes when we remove the last instance of C2, from Bool to [Char].)

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances, TypeFamilies #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE OverlappingInstances #-}

module FD where

class C1 a b | a -> b where foo :: a -> b

instance C1 [a] [a] where foo = id

instance C1 (Maybe a) (Maybe a) where foo = id

{- -- correctly prohibited! instance x ~ Bool => C1 [Char] x where foo = const True -}

t1 = foo "a" t11 = \x -> foo [x] -- t11 :: t -> [t]

-- Anthony Clayden's translation class C2 a b where foo2 :: a -> b

instance x ~ [a] => C2 [a] x where foo2 = id

instance x ~ (Maybe a) => C2 (Maybe a) x where foo2 = id

instance x ~ Bool => C2 [Char] x where foo2 = const True

t2 = foo2 "a" t21 = \x -> foo2 [x] -- t21 :: C2 [t] b => t -> b

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime