wiki:FunctionalDependencies

Version 10 (modified by ravi@…, 8 years ago) (diff)

--

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.

Details

Restrictions on classes and instances

The original paper imposed two restrictions on instances (sect. 6.1), stated here for the class C declared above:

  1. For any instance
    instance ... => C Ta Tb Tc
    
    any variable occurring free in Tb must also occur free in Ta.
  2. If there is a second instance
    instance ... => C Sa Sb Sc
    
    then any substitution unifying Ta and Sa must also unify Tb and Sb.

Haskell 98 requires that contexts of class and instance declarations may only use type variables that appear in the head. It was originally thought that this could be relaxed, to variables determined by those in the head, but this can lead to non-termination (CHR paper, ex. 15). With FlexibleInstances and no OverlappingInstances, these restrictions yield a coherent and decidable system (CHR paper, corr. 1).

However the first restriction forbids instances like the following from the monad transformer library:

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

GHC and Hugs accept this, because they relax the restriction by using dependency information from the context of the instance declaration. Unfortunately, this relaxation breaks the guarantees of termination (CHR paper, ex. 6) and coherence (CHR paper, ex. 18). This restriction and others may be safely relaxed in some circumstances, but no simple general rule is known.

Type inference

Again the implemented system is more powerful (and useful) than the specified one, e.g. the example in sect. 7 of the original paper.

Attachments (1)

Download all attachments as: .zip