Fundeps discrepancy

[Martin SULZMANN]

Hi,

Yes, there is a formal description of type inference for FDs. 
You can download a paper via 
http://www.comp.nus.edu.sg/~sulzmann/chr/publications.html
(Sound and Decidable Type Inference for Functional Dependencies
by  Gregory J. Duck, Simon Peyton-Jones, Peter J. Stuckey and Martin
Sulzmann)
which provides some formal results
under which conditions imposed on FDs type inference is sound and
decidable.

In fact, your example above is harmless in the sense that type
inference remains decidable. Although, we might lose completeness of type
inference (because the super class relations of the example below
are not range-restricted).

*Real* problems arise once we start writing the following

class C a b | a->b
instance C a b => C [a] [b]

The above program violates the "termination" condition as stated in
Mark Jones, ESOP 2000 paper.
Indeed, Hugs and GHC don't strictly enforce this condition, hence, we
might lose
decidability of type inference. Please consult the above mentioned paper for an
extensive discussion.

You (and Brandon Michael Moore and many, many others in some previous
emails) were also raising issues 
why some seemingly well-typed programs making use of FDs are currently 
rejected. As you know
the well-typing and evidence-translation of programs are intimately
tied together.
The point is that current implementations are simply too
conservative. Note that in the above mentioned paper we are only
concerned with typing issues. A description of a more *relaxed*
evidence-translation scheme
will be discussed in some future work.

Martin

 > Hello again,
 > 
 > Please pardon another question on functional dependencies.  GHC and Hugs
 > behave differently on the following code:
 > 
 >     class Tr tr a b | tr -> a b where f :: tr -> a -> b
 >     class (Tr m a b, Tr n b c) => TrPair m n a c
 > 
 > The type variable b on the second line does not appear in the head,
 > but is determined by m and n in the head via the functional dependency
 > declared for Tr.  Hugs accepts this code, while GHC doesn't.  The
 > original fundeps paper (Mark Jones, ESOP 2000) seems silent on this
 > point.
 > 
 > Taking a step back, is there a formal description of type inference for
 > functional dependencies in Haskell type classes?  A set of typing rules,
 > or something written along the lines of John Peterson and Mark Jones's
 > "Implementing type classes" (PLDI 1993) or Mark Jones's "Typing Haskell
 > in Haskell", would be wonderful to have.
 > 
 > 	Ken
 > 
 > -- 
 > Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
 > Tax the rich!
 > new journal Physical Biology: http://physbio.iop.org/
 > What if All Chemists Went on Strike? (science fiction):
 > http://www.iupac.org/publications/ci/2003/2506/iw3_letters.html
 > _______________________________________________
 > Haskell mailing list
 > Haskell at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell