Re: FunDeps: divergent improvement from overlapping instances

--===============8712069443604231601==
Content-Type: multipart/alternative; boundary="000000000000560b9e05e600c5be"

--000000000000560b9e05e600c5be
Content-Type: text/plain; charset="UTF-8"

> A precondition is that it scans instances in most-specific-first sequence
> -- which Hugs is already doing.

It galled me that going only by (an adapted notion of) overlap, I still had
to write three instances for a three-FunDep AddNat:

> class AddNat x y z | x y -> z, x z -> y, y z -> x
>
> instance AddNat Z Z Z
> instance AddNat Z (S y') (S y')
>
> instance AddNat x' y z' => AddNat (S x') y (S z')
>

because the 'obvious' way to write, with two instances (see below), put
them in no substitution ordering for the argument positions to the third
FunDep. So I dug out an idea from a few years ago (rejected proposal) and
implemented:

> instance  AddNat Z y y
>
> instance AddNat x' y z' => AddNat (S x') y (S z') | y /~ (S z')
>

That after the `|` in the instance is an 'Instance Disequality Guard':
prefer a more specific instance if those two types from the head unify.

Then Hugs puts that instance later in the preference ordering than the
first instance -- because the instance heads unify going by the argument
positions, but the first instance has no guard.

This also works for the semi-overlap instances that Hugs currently
rejects/GHC accepts but might turn out to be unusable:

>    class Semi a b
>
>    instance Semi Int b
>    instance Semi a   Bool  | a /~ Int
>
>    [W] Semi Int Bool             -- GHC currently rejects as ambiguous

The guard says: in case of [W] Semi Int Bool, prefer the Semi Int b
instance. We can even go:

>    instance Semi Int Bool
>
>    instance Semi Int b     | b /~ Bool
>    instance Semi a   Bool  | a /~ Int
>
>    instance Semi a  b             -- no guard, because strictly more
general than any instance

--000000000000560b9e05e600c5be
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div dir=3D"ltr">&gt;=C2=A0<span style=3D"color:rgb(0,0,0)=
;white-space:pre-wrap">A precondition is that it scans instances in </span>=
<span style=3D"color:rgb(0,0,0);white-space:pre-wrap">most-specific-first s=
equence</span><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">&g=
t; -- which Hugs is already doing.</span></div><div><span style=3D"color:rg=
b(0,0,0);white-space:pre-wrap"><br></span></div><div><span style=3D"color:r=
gb(0,0,0);white-space:pre-wrap">It galled me that going only by (an adapted=
 notion of) overlap, I still had to write three instances for a three-FunDe=
p AddNat:</span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-=
wrap"><br></span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre=
-wrap">&gt;    class AddNat x y z  | x y -&gt; z, x z -&gt; y, y z -&gt; x<=
/span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">&gt;=
</span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">&gt=
;    instance</span>

<span style=3D"color:rgb(0,0,0);white-space:pre-wrap">                 </sp=
an><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">AddNat Z     Z    =
  Z     </span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-w=
rap">&gt;    instance                  AddNat Z      (S y&#39;) (S y&#39;)<=
/span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">&gt;=
</span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">&gt=
;    instance AddNat x&#39; y z&#39; =3D&gt; AddNat (S x&#39;) y     (S z&#=
39;)</span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap"=
>&gt;</span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wrap=
"><br></span></div><div><span style=3D"color:rgb(0,0,0);white-space:pre-wra=
p">because the &#39;obvious&#39; way to write, with two instances (see belo=
w), put them in no substitution ordering for the argument positions to the =
third FunDep. So I dug out an idea from a few years ago (rejected proposal)=
 and implemented:</span></div><div><span style=3D"color:rgb(0,0,0);white-sp=
ace:pre-wrap"><br></span></div><div><span style=3D"color:rgb(0,0,0);white-s=
pace:pre-wrap">&gt;    </span><span style=3D"color:rgb(0,0,0);white-space:p=
re-wrap">instance</span>=C2=A0<span style=3D"color:rgb(0,0,0);white-space:p=
re-wrap">                 </span><span style=3D"color:rgb(0,0,0);white-spac=
e:pre-wrap">AddNat Z     y      y    </span></div><div><span style=3D"color=
:rgb(0,0,0);white-space:pre-wrap">&gt;</span></div><div><div><span style=3D=
"color:rgb(0,0,0);white-space:pre-wrap">&gt;    instance AddNat x&#39; y z&=
#39; =3D&gt; AddNat (S x&#39;) y     (S z&#39;)  | y /~ (S z&#39;)</span></=
div>&gt;</div><div><br></div><div>That after the `|` in the instance is an =
&#39;Instance Disequality Guard&#39;: prefer a more specific instance if th=
ose two types from the head unify.</div><div><br></div><div>Then Hugs puts =
that instance later in the preference ordering than the first instance -- b=
ecause the instance heads unify going by the argument positions, but the fi=
rst instance has no guard.</div><div><br></div><div>This also works for the=
 semi-overlap instances that Hugs currently rejects/GHC accepts but might t=
urn out to be unusable:</div><div><br></div><div>&gt;=C2=A0 =C2=A0 class Se=
mi a b</div><div>&gt;</div><div>&gt;=C2=A0 =C2=A0 instance Semi Int b</div>=
<div>&gt;=C2=A0 =C2=A0 instance Semi a=C2=A0 =C2=A0Bool=C2=A0 | a /~ Int</d=
iv><div>&gt;</div><div>&gt;=C2=A0 =C2=A0 [W] Semi Int Bool=C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0-- GHC currently rejects as ambiguous</div><=
div><br></div><div>The guard says: in case of [W] Semi Int Bool, prefer the=
 Semi Int b instance. We can even go:</div><div><br></div><div>&gt;=C2=A0 =
=C2=A0 instance Semi Int Bool</div><div>&gt;</div><div>&gt;=C2=A0 =C2=A0 in=
stance Semi Int b=C2=A0 =C2=A0 =C2=A0| b /~ Bool</div><div>&gt;=C2=A0 =C2=
=A0 instance Semi a=C2=A0 =C2=A0Bool=C2=A0 | a /~ Int</div><div>&gt;</div><=
div>&gt;=C2=A0 =C2=A0 instance Semi a=C2=A0 b=C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0-- no guard, because strictly more general than any ins=
tance</div><div><br></div><div><br></div></div><div class=3D"gmail_quote"><=
blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l=
eft:1px solid rgb(204,204,204);padding-left:1ex">
</blockquote></div></div>

--000000000000560b9e05e600c5be--

--===============8712069443604231601==
Content-Type: text/plain; charset="utf-8"
MIME-Version: 1.0
Content-Transfer-Encoding: base64
Content-Disposition: inline

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=

--===============8712069443604231601==--