Simon Peyton-Jones wrote:
Until now, no one has know how to combine fundeps and local constraints. For example
class C a b | a->b where op :: a -> b
instance C Int Bool where op n = n>0
data T a where T1 :: T a T2 :: T Int
-- Does this typecheck? f :: C a b => T a -> Bool f T1 = True f T2 = op 3
The function f "should" typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool). But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it.
At least for this particular example, a simple desugaring translation makes even GHC 6.10.4 accept the example. We first desugar GADT into the regular ADT and the EQ constraint (the process, as I understand, already happens under the hood). We then make use of that constraint.
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
module F where
class C a b | a->b where op :: a -> b
instance C Int Bool where op n = n>0
data EQ a b where Refl :: EQ a a
-- A primitive version of Leibniz substitution principle. cast :: EQ a b -> a -> b cast Refl x = x
-- Original GADT -- data T a where -- T1 :: T a -- T2 :: T Int
-- desugared version of T data TT a = TT1 | TT2 (EQ a Int)
g :: C a b => TT a -> Bool g TT1 = True g (TT2 eq) = op (if False then cast eq undefined else 3)
test1 = g (TT2 Refl)
It works. Martin Sulzmann wrote:
Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other.
As Martin himself said in the next paragraph of his message, the equivalence claim has an exception: overlapping instances. Functional dependencies do work with overlapping instances, but type families do not. That issue has been noted just the other month on this list. There is another exception. Let's consider type class C with a functional dependency, and a seemingly equivalent type family F.
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes, FunctionalDependencies #-}
module F1 where
class C a b | a->b instance C Int Bool
type family F a :: * type instance F Int = Bool
newtype N1 a = N1 (F a)
n1 :: N1 Int -> Bool n1 (N1 x) = x
t1 = n1 (N1 True)
newtype N2 a = N2 (forall b. C a b => b)
n2 :: N2 Int -> Bool n2 (N2 x) = x
-- t2 = n2 ((N2 True) :: N2 Int)
The code type checks. It seems that for each piece of code using C we can write an equivalent piece of code using F -- until we come to t1 and t2. If we uncomment the last line, we get a type error /tmp/c.hs:25:13: Couldn't match expected type `b' against inferred type `Bool' `b' is a rigid type variable bound by the polymorphic type `forall b. (C Int b) => b' at /tmp/c.hs:25:10 In the first argument of `N2', namely `True' In the first argument of `n2', namely `((N2 True) :: N2 Int)' In the expression: n2 ((N2 True) :: N2 Int) Although the type variable b must be Bool (since it is uniquely determined by the functional dependency C Int b), GHC can't see that.