The Sum class can be used to both add and substract.
class Sum a b c | a b -> c, a c -> b, b c -> a
TF are too strict
For example, you cannot recurse with If
type family If p a btype instance If HTrue a b = atype instance If HFalse a b = btype family Gcd a btype instance Gcd a b = If (IsZero b) a (Gcd b (Rem a b))
The type family has to use a helper TF (or in this case a plain type):
type Gcd a b = Gcd_helper (IsZero b) a btype family Gcd_helper p a btype instance Gcd_helper HTrue a b = atype instance Gcd_helper HFalse a b = Gcd b (Rem a b)
More complicated type-level programs get very ugly using this style.
The same If works in a class instance using constraint kinds.
class Gcd a b c | a b -> cinstance ( IsZero b p, If p (b ~ c) (Rem a b r, Gcd b r c)) => Gcd a b c
It is possible to partially apply class predicates using constraint kinds.
class F a b | a -> binstance F Int Charclass FMap (f :: * -> * -> Constraint) a b | f a -> binstance (f a b) => FMap f (HJust a) (HJust b)x = undefined :: FMap F (HJust Int) a => a
But type families cannot be partially applied (Type synonym F' should have 1 argument, but has been given none):
type family FMap (f :: * -> *) atype instance FMap f (HJust a) = HJust (f a)type family F atype instance F Int = Charx = undefined :: FMap F (HJust Int)
The standard encoding of the above class from FD to
superclass equalities does not work because type instances
can't have type variables on the RHS which weren't introduced
in the LHS:
class (f :<$>: a) ~ b => FMap (f :: * -> * -> Constraint) a b where type f :<$>: ainstance f a b => FMap f (HJust a) (HJust b) where type f :<$>: (HJust a) = HJust b -- error, b not available
No overlapping type instances
IsZero for two's complement integers is longer than it could be.
type family IsZero itype instance IsZero Zeros = True-- type instance IsZero i = Falsetype instance IsZero Ones = Falsetype instance IsZero Zero = Falsetype instance IsZero One = False
MonadState cannot be implemented easily without overlap. It works with FD.
class Monad m => MonadState s m | s -> m where get :: m s put :: s -> m ()instance (Monad m) => MonadState s (StateT s m) where get = StateT $ \s -> return (s, s)instance (Monad (t m), MonadTrans t, MonadState s m) => MonadState s (t m) where get = lift get put = lift . put
But not with TF.
class (Monad m) => MonadState m where type MonadStateType m get :: m (MonadStateType m) put :: (MonadStateType m) -> m ()instance (Monad m) => MonadState (StateT s m) where type MonadStateType (StateT s m) = s get = StateT $ \s -> return (s, s) put s = StateT $ \_ -> return ((), s)instance (Monad (t m), MonadTrans t, MonadState m) => MonadState (t m) where type MonadStateType (t m) = MonadStateType m get = lift get put = lift . put
The new Nat kind contains an unlimited amount of types. Overlapping
type instances are needed to write total type instances that don't use
the built-in solver.
type family F (a :: Nat)type instance F 0 = ...type instance F 1 = ...type instance F 2 = ......-- type instance F n = ...
This does not work (Conflicting family instance declarations).
type family TypeEq a btype instance TypeEq a a = HTruetype instance TypeEq a b = HFalse
But this does.
class TypeEq a b p | a b -> pinstance TypeEq a a HTrueinstance false ~ HFalse => TypeEq a b false
* GADTs: - GADTs and FDs generally can't be mixed (well, you can mix them, and when a program compiles, it is type correct, but a lot of type correct programs will not compile) - GADTs and TFs work together just fine* Existential types: - Don't work properly with FDs; here is an example: class F a r | a -> r instance F Bool Int data T a = forall b. F a b => MkT b add :: T Bool -> T Bool -> T Bool add (MkT x) (MkT y) = MkT (x + y) -- TYPE ERROR - Work fine with TFs; here the same example with TFs type family F a type instance F Bool = Int data T a = MkT (F a) add :: T Bool -> T Bool -> T Bool add (MkT x) (MkT y) = MkT (x + y) (Well, strictly speaking, we don't even need an existential here, but more complicated examples are fine, too.)
Type-level programming with TF is generally nicer
Type-level programming with classes looks like an ugly Prolog,
while similar code using TF looks more functional and has no free
The class instance being defined is unhelpfully placed after the
class Minus (a :: k) (b :: k) (dif :: k) | a b -> difinstance ( Negate b nb, (a + nb) dif) => Minus a b dif
type family (a :: k) `Minus` (b :: k) :: ktype instance a `Minus` b = a + Negate b
FD are not real FD, they only help pick instances
The result of a class constraint is not obvious.
C a b could have the FD a -> b, b -> a, neither, both or even someting like
-> a b. Looking at the :info doesn't always help to figure out the
resulting FD of a class. The kind of a class does not include the
FD. There is also no FD inference.
>>> class C a b | a -> b>>> class C a b => C' a b>>> :i C'class C a b => C' a b>>> :k CC :: * -> * -> Constraint
With constraint kinds, a constraint can be an open type family. There is no
way at all of telling what its FD are.