Functional dependencies and improvement
Hi, yet again FD's! In my previous example I employed FD's to improve constraints. However, there are cases where FD's seem to be overly restrictive. Take a look at the Haskell code below. Have others made similar experiences? Martin -- FDs are sometimes overly restrictive module Insert where class Insert a b | b -> a where insert :: a->b->b class Leq a where leq :: a->a->Bool instance Leq a => Insert a [a] -- we're not so interested in the values for the purpose of this example -- hugs or ghc will complain about the following instance instance Insert Int [Float] -- though this makes sense! Elements of value Int should allowed to be stored as Floats {- Reason: Improvement in case of FDs seems overly restrictive Consider Mark Jones paper "Type Classes with Functional Dependencies", page 12, Section 6.2. In case of the above type class we require that for each constraint Insert t1 t2 and declaration instance C => Insert t1' t2' where if phi(t2) = t2' then phi(t1) = t1' for some substitution phi. However, we have that phi([a]) = [Float] and phi(a) \not= Int where phi=[a |-> Float]. The problem is that the improvement strategy does not take into account the context in the instance declaration. Solution: We should only improve 'Insert a [b]' to 'Insert b [b]' where phi=[a |-> b] in case we additionally find 'Leq b'. Though, this cannot be specified with FD's. -}
Martin, | In my previous example I employed FD's to | improve constraints. However, there are cases where FD's seem | to be overly restrictive. Yes, of course! So it will be for any extension of the type system that retains both decidability and soundness. The particular form of "improvement" that is provided by FDs represents an engineering trade off, supporting some useful examples while requiring only a relatively modest extension to the syntax and semantics of the language. They do not (and were never intended to) provide a universal tool that can handle all possible refinements of type inference with classes. More specialized forms of improvement, including instance specific rules, have been described elsewhere. My paper on improvement [1] provides a framework for this and hints at some examples. (In fact I think there is another example buried in comments in the source code for Hugs that few people have probably ever seen ... assuming that the current maintainers haven't had any reason to take it out! If you're really curious, look in subst.c ...) All the best, Mark [1] Simplifying and Improving Qualified Types http://www.cse.ogi.edu/~mpj/pubs/improve.html
participants (2)
-
Mark P Jones -
Martin Sulzmann