Changes between Version 8 and Version 9 of FunctionalDependencies


Ignore:
Timestamp:
Feb 5, 2006 1:41:14 AM (10 years ago)
Author:
ross@…
Comment:

details from CHR paper

Legend:

Unmodified
Added
Removed
Modified
  • FunctionalDependencies

    v8 v9  
    44== Brief Explanation ==
    55
     6Functional dependencies (borrowed from relational databases) are a partial solution to the ambiguities that plague [wiki:MultiParamTypeClasses multi-parameter type classes], e.g.
     7{{{
     8class ... => C a b c | a -> b
     9}}}
     10says that any two instances of `C` that agree in the first parameter must also agree in the second.
     11
    612== References ==
    7  * [http://www.cse.ogi.edu/~mpj/pubs/fundeps.html Type Classes with Functional Dependencies] (paper) by Mark P. Jones, in ESOP 2000. A semi-formal description of a more restricted system than implemented by GHC and Hugs.
    8  * [http://research.microsoft.com/Users/simonpj/Papers/fd-chr/ Sound and Decidable Type Inference for Functional Dependencies] by Gregory J. Duck, Simon Peyton Jones, Peter J. Stuckey and Martin Sulzmann, in ESOP 2004. ([http://www.comp.nus.edu.sg/~sulzmann/chr/download/fd-chr.ps.gz extended version])
    9  * [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#functional-dependencies Description] from the GHC User's manual.
     13 * [http://www.cse.ogi.edu/~mpj/pubs/fundeps.html Type Classes with Functional Dependencies] by Mark P. Jones, in ESOP 2000. A semi-formal description of a more restricted system than implemented by GHC and Hugs.
     14 * [http://research.microsoft.com/Users/simonpj/Papers/fd-chr/ Understanding functional dependencies via Constraint Handling Rules] by Martin Sulzmann, Gregory J. Duck, Simon Peyton Jones, and Peter J. Stuckey, September 2005.
     15 * [http://cvs.haskell.org/Hugs/pages/hugsman/exts.html#sect7.1.1 Multiple parameter classes] in the Hugs 98 User Manual
    1016 * [http://www.haskell.org/pipermail/haskell/2000-December/006324.html Problem] with functional dependencies (email) by Simon Peyton Jones - is there a conclusion here? Further work?
    1117
     
    1521== Pros ==
    1622 * In GHC and Hugs for a long time.
     23 * Used in important libraries, notably monad transformers.
     24 * MultiParamTypeClasses are of limited use without functional dependencies or something equivalent.
    1725
    1826== Cons ==
    19  * Recently, some problems with FDs have been identified, see also the material on AssociatedTypes.
    20  * There are (at least) three different versions of FDs:
    21    1. Mark Jones' original proposal.  Problem: It excludes some uses of FDs.
    22    2. GHC's implementation.  Problem: It makes type checking undecidable.  (See Duck et al. for an example.)
     27 * There are (at least) three different versions of FDs, none of which is satisfactory:
     28   1. Mark Jones's original proposal.  Problem: It excludes some uses of FDs (see below).
     29   2. GHC's implementation.  Problem: It makes type checking undecidable (see below).
    2330   3. Chameleon's implementation.  Problem: Needs type inference based on constraint handling rules (not just HM).  Doesn't support separate compilation atm.
     31 * Including the dependent type parameters makes types more cluttered, and prevents hiding of these types (see AssociatedTypes).
     32 * AssociatedTypes seem to be more promising.
     33
     34== Details ==
     35
     36=== Restrictions on classes and instances ===
     37
     38The original paper imposed two restrictions on instances (sect. 6.1), stated here for the class `C` declared above:
     39
     40 1. For any instance
     41    {{{
     42instance ... => C Ta Tb Tc
     43}}}
     44    any variable occurring free in Tb must also occur free in Ta.
     45 2. If there is a second instance
     46    {{{
     47instance ... => C Sa Sb Sc
     48}}}
     49    then any substitution unifying Ta and Sa must also unify Tb and Sb.
     50
     51Haskell 98 requires that contexts of class and instance declarations may only use type variables that appear in the head.
     52It 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).
     53With FlexibleInstances and no OverlappingInstances, these restrictions yield a coherent and decidable system (CHR paper, corr. 1).
     54
     55However the first restriction forbids instances like the following from the monad transformer library:
     56{{{
     57class (Monoid w, Monad m) => MonadWriter w m | m -> w
     58instance MonadWriter w m => MonadWriter w (ReaderT r m)
     59}}}
     60GHC and Hugs accept this, because they relax the restriction by using dependency information from the context of the instance declaration.
     61Unfortunately, this relaxation breaks the guarantees of termination (CHR paper, ex. 6) and coherence (CHR paper, ex. 18).
     62This restriction and others may be safely relaxed in some circumstances, but no simple general rule is known.
     63
     64=== Type inference ===
     65
     66Again the implemented system is more powerful (and useful) than the specified one, e.g. the example in sect. 7 of the original paper.