Sorry, forgot to add [2] http://www.comp.nus.edu.sg/~sulzmann/publications/jfp-fds-revised.pdf Martin Martin Sulzmann writes:
Mark P Jones writes:
[Sorry, I guess this should have been in the cafe ...]
Simon Peyton-Jones wrote:
The trouble is that a) the coverage condition ensures that everything is well behaved b) but it's too restrictive for some uses of FDs, notably the MTL library c) there are many possibilities for more generous conditions, but the useful ones all seem complicated
Concerning the last point I've dumped the current brand leader for (c) into http://hackage.haskell.org/trac/ghc/ticket/1241#comment:15.
Better ideas for (c) would be welcome.
Let's take the declaration: "instance P => C t where ..." The version of the "coverage condition" in my paper [1] requires that TV(t_Y) \subseteq TV(t_X), for each dependency (X->Y) \in F_C. (I'm using the notation from the paper; let me know if you need more help to parse it.) This formulation is simple and sound, but it doesn't use any dependency information that could be extracted from P. To remedy this, calculate L = F_P, the set of functional dependencies induced by P, and then expand the right hand side of the set inequality above by taking the closure of TV(t_X) with respect to L. In symbols, we have to check that:
TV(t_Y) \subseteq TV(t_X)^+_L, for each (X->Y) \in F_C.
I believe (but haven't formally proved) that this is sound; I don't know how to make a more general "coverage condition" without losing that. I don't know if it's sufficient for examples like MTL (because I'm not sure where to look for details of what that requires), but if it isn't then I'd be very suspicious ...
All the best, Mark
I think the above is equivalent to the (refined) weak coverage condition in [2] (see Section 6, p26). The weak coverage condition give us soundness. More precisely, we obtain confluence from which we can derive consistency (which in turn guarantees that the type class program is sound).
*BUT* this only works if we have termination which is often very tricky to establish.
For the example,
class Concrete a b | a -> b where bar :: a -> String
instance (Show a) => Concrete a b
termination holds, but the weak coverage condition does *not* hold. Indeed, this program should be therefore rejected.
Martin _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe