Martin Sulzmann sulzmann at comp.nus.edu.sg
Thu Oct 18 03:36:26 EDT 2007

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
> _______________________________________________