Version 10 (modified by 11 years ago) (diff)  ,

Functional Dependencies
Brief Explanation
Functional dependencies (borrowed from relational databases) are a partial solution to the ambiguities that plague multiparameter 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
 Type Classes with Functional Dependencies by Mark P. Jones, in ESOP 2000. A semiformal description of a more restricted system than implemented by GHC and Hugs.
 Understanding functional dependencies via Constraint Handling Rules by Martin Sulzmann, Gregory J. Duck, Simon Peyton Jones, and Peter J. Stuckey, September 2005. This paper explains explores the restrictions required to guarantee sound, complete and decidable type inference in the presence of functional dependencies.
 Multiple parameter classes in the Hugs 98 User Manual
 Problem with functional dependencies (email) by Simon Peyton Jones  is there a conclusion here? Further work?
Tickets
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:
 Mark Jones's original proposal. Problem: It excludes some uses of FDs (see below).
 GHC's implementation. Problem: It makes type checking undecidable (see below).
 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:
 For any instance
instance ... => C Ta Tb Tc
any variable occurring free in Tb must also occur free in Ta.  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 nontermination (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)

thoughtsOnMixing.ps (87.2 KB)  added by 11 years ago.
possible use case for FunctionalDependencies
Download all attachments as: .zip