Hugs/Trex and Overlapping Instances and FunDeps

Anthony Clayden <[email protected]> Tue, 27 Sep 2022 19:26:16 +1300
Newsgroups gmane.comp.lang.haskell.hugs.user
Message-ID <CABU_mxgqTxJA_E=-ngvjjD0c2K3dyG+hctMuZemNVuCA0xx6cA@mail.gmail.com>
--===============3090540752906508994==
Content-Type: multipart/alternative; boundary="00000000000058515f05e9a2b9fe"

--00000000000058515f05e9a2b9fe
Content-Type: text/plain; charset="UTF-8"

I decided this could usefully be a feature, rather than a bug:
https://mail.haskell.org/pipermail/hugs-bugs/2022-September/001929.html

So I meshed it with work-in-progress on overlaps; and on allowing instances
inconsistent with FunDeps providing an overlap is strictly more specific;
and in looking to FunDep's determining positions only for detecting
overlap. So this now is accepted (`trexRemv` returns its first argument,
removing any fields whose labels are common with its second arg):


>
>    import Hugs.Trex
>
>    class TrexRemv r1 r2 rr  | r1 r2 -> rr  where
>        trexRemv :: Rec r1 -> Rec r2 -> Rec rr
>
>    instance TrexRemv EmptyRow r2 EmptyRow  where
>        trexRemv _empty _r2 = emptyRec
>
>    instance (r1'\x, r2'\x, TrexRemv r1' ( x :: _b | r2') rr', rr'\x )
>             => TrexRemv ( x :: a | r1') ( x :: _b | r2') rr'
>      where
>        trexRemv ( x = x | r1') r2 = trexRemv r1' r2
>
>    instance (r1'\x, r2\x, TrexRemv r1' r2 rr', rr'\x )
>             => TrexRemv ( x :: a | r1') r2 ( x :: a | rr' )
>      where
>        trexRemv ( x = x | r1') r2 = ( x = x | trexRemv r1' r2 )
>
>    instance (r1'\y, r2'\y, TrexRemv r1' ( y :: _b | r2') rr', rr'\y )
>             => TrexRemv ( y :: a | r1') ( y :: _b | r2') rr'
>      where
>        trexRemv ( y = y | r1') r2 = trexRemv r1' r2
>
>    instance (r1'\y, r2\y, TrexRemv r1' r2 rr', rr'\y )
>             => TrexRemv ( y :: a | r1') r2 ( y :: a | rr' )
>      where
>        trexRemv ( y = y | r1') r2 = ( y = y | trexRemv r1' r2 )
>


For each specific label, the instance heads overall are in no substitution
ordering -- because the label appears in the result just in case it
_doesn't_ appear in the second arg. The new rule is to consider only the
argument (first two) positions.

For each distinct label, the heads unify: the common instance has both
labels. The new rule is that if heads differ in having distinct labels in
corresponding positions, treat them as apart. (Or equivalently treat them
as overlapping in strict alphabetic order of labels. So you can write
instances in any sequence; they'll get loaded to alpha seq.)

As I said in that maybe-bug report


>>
>> it's Trex where records are considered isomorphic up to permutation of
labels;
>> and because each instance has an `EqRecRow b` constraint for the rest of
the row;
>> it doesn't matter how Hugs resolves the wanted to the instances
>>

[s/EqRecRow/TrexRemv/]


Similar to `remv` there's classes for `proj`(ect) and `app`(end) of rows
with distinct labels, needing these overlap rules.

So along with the Trex syntax for rows, I now have an expressively complete
set of operations. Nice-to-have would be generating these instances
on-the-fly -- as Hugs does for `Eq, Show`. That looks hard.

AntC

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

<div dir=3D"ltr"><div><br></div>I decided this could usefully be a feature,=
 rather than a bug:<div><a href=3D"https://mail.haskell.org/pipermail/hugs-=
bugs/2022-September/001929.html">https://mail.haskell.org/pipermail/hugs-bu=
gs/2022-September/001929.html</a><br></div><div><br></div><div>So I meshed =
it with work-in-progress on overlaps; and on allowing instances inconsisten=
t with FunDeps providing an overlap is strictly more specific; and in looki=
ng to FunDep&#39;s determining positions only for detecting overlap. So thi=
s now is accepted (`trexRemv` returns its first argument, removing any fiel=
ds whose labels are common with its second arg):</div><div><br></div><div><=
br></div><div>&gt;</div>&gt;=C2=A0 =C2=A0 import Hugs.Trex<br><div>&gt;</di=
v><div>&gt;=C2=A0 =C2=A0 class TrexRemv r1 r2 rr =C2=A0| r1 r2 -&gt; rr =C2=
=A0where<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=A0=C2=A0trexRemv :: Rec r1 -&gt; R=
ec r2 -&gt; Rec rr<br>&gt;=C2=A0 =C2=A0=C2=A0<br>&gt;=C2=A0 =C2=A0 instance=
 TrexRemv EmptyRow r2 EmptyRow =C2=A0where<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=
=A0=C2=A0trexRemv _empty _r2 =3D emptyRec<br>&gt;=C2=A0=C2=A0<br>&gt;=C2=A0=
 =C2=A0 instance (r1&#39;\x, r2&#39;\x, TrexRemv r1&#39; ( x :: _b | r2&#39=
;) rr&#39;, rr&#39;\x )<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0=3D&gt; TrexRemv ( x :: a | r1&#39;) ( x :: _b | r2&#39;) rr&#39; <br=
>&gt;=C2=A0 =C2=A0 =C2=A0 where=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0<br>&gt;=C2=A0 =C2=A0 =C2=
=A0 =C2=A0 trexRemv ( x =3D x | r1&#39;) r2 =3D trexRemv r1&#39; r2 <br>&gt=
;=C2=A0=C2=A0<br>&gt;=C2=A0 =C2=A0 instance (r1&#39;\x, r2\x, TrexRemv r1&#=
39; r2 rr&#39;, rr&#39;\x )<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0=3D&gt; TrexRemv ( x :: a | r1&#39;) r2 ( x :: a | rr&#39; )=C2=
=A0<br>&gt;=C2=A0 =C2=A0 =C2=A0 where<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=A0 tr=
exRemv ( x =3D x | r1&#39;) r2 =3D ( x =3D x | trexRemv r1&#39; r2 )<br>&gt=
;<br>&gt;=C2=A0 =C2=A0 instance (r1&#39;\y, r2&#39;\y, TrexRemv r1&#39; ( y=
 :: _b | r2&#39;) rr&#39;, rr&#39;\y )<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0=3D&gt; TrexRemv ( y :: a | r1&#39;) ( y :: _b | r2&#39=
;) rr&#39; <br>&gt;=C2=A0 =C2=A0 =C2=A0 where<br>&gt;=C2=A0 =C2=A0 =C2=A0 =
=C2=A0 trexRemv ( y =3D y | r1&#39;) r2 =3D trexRemv r1&#39; r2<br>&gt;=C2=
=A0=C2=A0<br>&gt;=C2=A0 =C2=A0 instance (r1&#39;\y, r2\y, TrexRemv r1&#39; =
r2 rr&#39;, rr&#39;\y )<br>&gt;=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0=3D&gt; TrexRemv ( y :: a | r1&#39;) r2 ( y :: a | rr&#39; ) =C2=A0<b=
r>&gt;=C2=A0 =C2=A0 =C2=A0 where=C2=A0 =C2=A0<br>&gt;=C2=A0 =C2=A0 =C2=A0 =
=C2=A0 trexRemv ( y =3D y | r1&#39;) r2 =3D ( y =3D y | trexRemv r1&#39; r2=
 )<br></div><div>&gt;</div><div><br></div><div><br></div><div>For each spec=
ific label, the instance heads overall are in no substitution ordering -- b=
ecause the label appears in the result just in case it _doesn&#39;t_ appear=
 in the second arg. The new rule is to consider only the argument (first tw=
o) positions.</div><div><br></div><div>For each distinct label, the heads u=
nify: the common instance has both labels. The new rule is that if heads di=
ffer in having distinct labels in corresponding positions, treat them as ap=
art. (Or equivalently treat them as overlapping in strict alphabetic order =
of labels. So you can write instances in any sequence; they&#39;ll get load=
ed to alpha seq.)</div><div><br></div><div>As I said in that maybe-bug repo=
rt</div><div><br></div><div><br></div><div>&gt;&gt;</div><div>&gt;&gt;=C2=
=A0<span style=3D"color:rgb(0,0,0);white-space:pre-wrap">it&#39;s Trex wher=
e records are considered isomorphic up to </span><span style=3D"color:rgb(0=
,0,0);white-space:pre-wrap">permutation of labels;</span></div><div><span s=
tyle=3D"color:rgb(0,0,0);white-space:pre-wrap">&gt;&gt; and because each in=
stance has an `EqRecRow b` </span><span style=3D"color:rgb(0,0,0);white-spa=
ce:pre-wrap">constraint for the rest of the row;</span></div><div><span sty=
le=3D"color:rgb(0,0,0);white-space:pre-wrap">&gt;&gt; it doesn&#39;t matter=
 how Hugs resolves the </span><span style=3D"color:rgb(0,0,0);white-space:p=
re-wrap">wanted to the instances</span></div><div><span style=3D"color:rgb(=
0,0,0);white-space:pre-wrap">&gt;&gt;</span></div><div><span style=3D"color=
:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style=3D"colo=
r:rgb(0,0,0);white-space:pre-wrap">[s/EqRecRow/TrexRemv/]</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"><br></span></div><di=
v><span style=3D"color:rgb(0,0,0);white-space:pre-wrap">Similar to `remv` t=
here&#39;s classes for `proj`(ect) and `app`(end) of rows with distinct lab=
els, needing these overlap rules.</span></div><div><span style=3D"color:rgb=
(0,0,0);white-space:pre-wrap"><br></span></div><div><span style=3D"color:rg=
b(0,0,0);white-space:pre-wrap">So along with the Trex syntax for rows, I no=
w have an expressively complete set of operations. Nice-to-have would be ge=
nerating these instances on-the-fly -- as Hugs does for `Eq, Show`. That lo=
oks hard.</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">AntC</span></div><div><br></div></div>

--00000000000058515f05e9a2b9fe--

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

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=

--===============3090540752906508994==--