(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,
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