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 > > > > [1] http://www.cs.pdx.edu/~mpj/pubs/fundeps-esop2000.pdf > > > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
