FDs and confluence
ross at soi.city.ac.uk
Mon Apr 10 06:27:14 EDT 2006
On Mon, Apr 10, 2006 at 05:49:15PM +0800, Martin Sulzmann wrote:
> Ross Paterson writes:
> > 1) consider the two constraint sets equivalent, since they describe
> > the same set of ground instances, or
> That's troublesome for (complete) type inference.
> Two constraint stores are equivalent if they are equivalent
> for any satisfying ground instance? How to check that?
You can't check it; it has to be proven for the system.
> I'm not following you here, you're saying?
> rule C [a] b d ==> d=Bool
> Are you sure that you're not introducing further "critical pairs"?
I don't see how -- there are no new redexes. Instance improvement was
already applicable, but now it has a different output.
> Maybe, you found a "simple" solution (that would be great)
> but I'not 100% convinced yet.
> The problem you're addressing only arises for non-full FDs.
> Aren't such cases very rare in practice?
My aim is not coverage but simplicity of description, and this version
still isn't simple enough.
More information about the Haskell-prime