wiki:FunctionalDependencies

Version 14 (modified by ross@…, 8 years ago) (diff)

fix ref

Functional Dependencies

Brief Explanation

Functional dependencies (borrowed from relational databases) are a partial solution to the ambiguities that plague multi-parameter type classes, e.g.

class ... => C a b c | a -> b

says that any two instances of C that agree in the first parameter must also agree in the second.

References

Tickets

#36
add FunctionalDependencies
#90
solve the MultiParamTypeClassDilemma

Pros

  • In GHC and Hugs for a long time.
  • Used in important libraries, notably monad transformers.
  • MultiParamTypeClasses are of limited use without functional dependencies or something equivalent.

Cons

  • There are (at least) three different versions of FDs, none of which is satisfactory:
    1. Mark Jones's original proposal. Problem: It excludes some uses of FDs (see below).
    2. GHC's implementation. Problem: It makes type checking undecidable (see below).
    3. Chameleon's implementation. Problem: Needs type inference based on constraint handling rules (not just HM). Doesn't support separate compilation atm.
  • Including the dependent type parameters makes types more cluttered, and prevents hiding of these types (see AssociatedTypes).
  • AssociatedTypes seem to be more promising.

Variations

Original version

Suppose a class C has a functional dependency X -> Y. The original paper imposed two restrictions on instances of the class C (sect. 6.1):

  1. For any instance
    instance ... => C t
    
    any variable occurring free in tY must also occur free in tX.
  2. If there is a second instance
    instance ... => C s
    
    then any substitution unifying tX with sX must also unify tY with sY.

Haskell 98 requires that the context of an instance declaration use only type variables that appear in the head. It was originally thought that this could be relaxed (original paper, sect. 6.3), to variables determined by those in the head, but this can lead to non-termination (CHR paper, ex. 16).

With FlexibleInstances and no OverlappingInstances, these restrictions yield a coherent and decidable system (CHR paper, corr. 1).

GHC and Hugs

GHC and Hugs implement a relaxed version of the first restriction above: they require only that any variable occurring free in tY be dependent (using dependencies of classes in the context) on variables that occur free in tX. They thus accept instances like the following from the monad transformer library, which is invalid according to the original rules:

class (Monoid w, Monad m) => MonadWriter w m | m -> w
instance MonadWriter w m => MonadWriter w (ReaderT r m)

Unfortunately, this relaxation breaks the guarantees of termination and coherence:

  • The following instances (CHR paper, ex. 6) seem reasonable:
    class Mul a b c | a b -> c where
            (.*.) :: a -> b -> c
    
    instance Mul Int Int Int where (.*.) = (*)
    instance Mul Int Float Float where x .*. y = fromIntegral x * y
    instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
    
    and yet instance inference fails to terminate for the following (erroneous) definition:
    f = \ b x y -> if b then x .*. [y] else y
    
  • The following instances (adapted from CHR paper, ex. 18) are sensitive to the order in which rules are applied:
    class B a b | a -> b
    class C a b | a -> b
    class D a b c | a -> b where f :: a -> b -> c -> Bool
    
    instance B a b => D [a] [b] Bool
    instance C a b => D [a] [b] Char
    
    Given the constraint D [a] [b] Bool, D [a] [c] Char,
    • if we apply the dependency first, and then reduce using the instances, we obtain b = c, B a b, C a b.
    • if we first reduce using the instances, we obtain B a b, C a c.
    (GHC and Hugs yield the former, because they defer context reduction: see FlexibleContexts).

New version

The following complex relaxation of the first rule is safe (CHR paper, sect. 6), and allows the instances in the monad transformer library:

  1. For any instance
    instance ... => C t
    
    either
    • any variable occurring free in tY must also occur free in tX, or
    • the functional dependency is full (involves all the arguments of the class), and the arguments tY are type variables determined by the free variables of tX.

Note that functional dependencies corresponding to associated type synonyms are always full.

Attachments (1)

Download all attachments as: .zip