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 > [EMAIL PROTECTED] > http://www.haskell.org/mailman/listinfo/haskell _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
