Is it time to start deprecating FunDeps?

[Martin Sulzmann]

(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,  <oleg at okmij.org> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime