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

[Iavor Diatchki]

Hello,

I believe that this "weak coverage condition" (which is also called
"the dependency condition" somewhere on the wiki) is exactly what GHC
6.4 used to implement but than in 6.6 this changed.  According to
Simon's comments on the trac ticket, this rule requires FDs to be
"full" to preserve the confluence of the system that is described in
the "Understanding Fds via CHRs" paper.  I have looked at the paper
many times, and I am very unclear on this point, any enlightenment
would be most appreciated (by the way, there was a post about that on
the haskell-prime list a couple of days ago, which contains a concrete
example as well).

To answer Mark's question, this rule provides enough power for mtl and
monadLib.  They use classes like "class StateM m s | m -> s" and
instances like "instance StateM m s => StateM (ExceptionT m) s".  (The
full source code for monadLib is at
http://www.galois.com/~diatchki/monadLib/monadLib-3.3.0/src/MonadLib.hs)

Martin, could you elaborate on the problem with non-termination?  I
have seen examples where the type-checker could loop while trying to
prove things, but I was not aware that there were implications related
to soundness as well.

-Iavor


On 10/18/07, Martin Sulzmann <sulzmann at comp.nus.edu.sg> wrote:
> 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
>