[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping
instances: a bug?]
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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list