Version 1 (modified by atnnn, 3 years ago) (diff) |
---|

# Type Families (TF) vs Functional Dependencies (FD)

I've gathered here some comments from the web and some of my personal experiences concerening the advantages and disadvantages of TF and FD over one another.

## Advantages of Functional Dependencies

### Mutual dependencies

TF are one way type functions, but a class can have multiple FD such as in

http://okmij.org/ftp/Haskell/PeanoArithm.lhs

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 b type instance If HTrue a b = a type instance If HFalse a b = b type family Gcd a b type 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 b type family Gcd_helper p a b type instance Gcd_helper HTrue a b = a type 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 -> c instance ( IsZero b p, If p (b ~ c) (Rem a b r, Gcd b r c)) => Gcd a b c

### Partial application

It is possible to partially apply class predicates using constraint kinds.

class F a b | a -> b instance F Int Char class FMap (f :: * -> * -> Constraint) a b | f a -> b instance (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 :: * -> *) a type instance FMap f (HJust a) = HJust (f a) type family F a type instance F Int = Char x = undefined :: FMap F (HJust Int)

Type synonyms can manipulate constraint kinds but can not use them. The following code doesn't make sense.

class (f :<$>: a) ~ b => FMap (f :: * -> * -> Constraint) a b where type f :<$>: a instance FMap f (HJust a) b where type f :<$>: (HJust a) = f a b => b

### No overlapping type instances

#### Identical alternatives

`IsZero` for two's complement integers is longer than it could be.

type family IsZero i type instance IsZero Zeros = True -- type instance IsZero i = False type instance IsZero Ones = False type instance IsZero Zero = False type 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

#### Nat

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 = ...

`TypeEq`

This does not work (`Conflicting family instance declarations`).

type family TypeEq a b type instance TypeEq a a = HTrue type instance TypeEq a b = HFalse

But this does.

class TypeEq a b p | a b -> p instance TypeEq a a HTrue instance false ~ HFalse => TypeEq a b false

#### See Also

### See Also

## Advantages of Type Families

### GADTs and existential types

From Manuel M T Chakravarty on Sun Feb 15 22:02:48 EST 2009

http://www.haskell.org/pipermail/haskell-cafe/2009-February/055890.html

* 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 variables.
- The class instance being defined is unhelpfully placed after the constraints.

class Minus (a :: k) (b :: k) (dif :: k) | a b -> dif instance ( Negate b nb, (a + nb) dif) => Minus a b dif

type family (a :: k) `Minus` (b :: k) :: k type 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 C C :: * -> * -> Constraint

With constraint kinds, a constraint can be an open type family. There is no way at all of telling what its FD are.

`UndecidableInstances` allows instances that violate the FD (#1241, #2247)

class F a b | a -> b where f :: (a,b) instance F Int b

Allows F Int Bool and F Int Char.

#### FD don't provide evidence (#4894)

class F a b | a -> b f :: (F a b, F a c) => a -> b -> c f _ = id

Gives the error

Could not deduce (b ~ c)

#### See also

## Converting from FD to TF

The standard encoding of FD using TF is:

With FD

class C a b | a -> b

With TF

class (F a ~ b) => C a b where type F a

Examples:

## See Also

- http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
- http://research.microsoft.com/en-us/um/people/simonpj/papers/fd-chr/
- TypeFunctions
- TypeFunctionsStatus
- TypeFunctions/IntegratedSolver
- http://www.haskell.org/haskellwiki/GHC/Indexed_types
- http://blog.omega-prime.co.uk/?p=127
- http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
- http://www.haskell.org/pipermail/haskell-prime/2011-June/003423.html
- http://code.atnnn.com/projects/type-prelude/wiki