[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]

[Martin Sulzmann]

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
 > Haskell-Cafe at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell-cafe