generic operations on Trex records [was: [haskell-beginners] Lifting over record syntax]
Anthony Clayden <[email protected]> Mon, 5 Nov 2018 00:55:22 +1300
| Newsgroups | gmane.comp.lang.haskell.hugs.user |
|---|---|
| Message-ID | <CAM7nRYSFVwAKEVE0fDaCQZ_bj7Lq_jckUyw5e4gPoKhCJXyw7Q@mail.gmail.com> |
--===============5149005072537840277==
Content-Type: multipart/alternative; boundary="00000000000030b6de0579d5729a"
--00000000000030b6de0579d5729a
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
On Thu, 1 Nov 2018 at 12:31 AM, Anthony Clayden wrote:
> Label names in Trex are literals; there's no such thing as a label
> variable. (Which is why it's a tad annoying that they start lower case.)
> Furthermore the same label name must appear in both terms and types -- in
> fact labels occupy a namespace separate vs terms or types. So Trex is a
> long way from from generic record handling like:
>
> recAppend :: ( rho'\__x ) =3D> Rec rho' -> Rec ( __x :: a) -> Rec ( __x :=
: a
> | rho')
> recAppend rho ( __x =3D x ) =3D ( __x =3D x | rho )
>
> in which I've used double-underscore prefix to signify a label variable.
> This is intended to extend a record `rho` with a singleton record. If we
> try appending a record with more than one field, beware that field order =
is
> arbitrary, so this
>
> recAppend rho ( __x =3D x, __y =3D y) =3D ...
>
> has no principal type (a familiar difficulty). The programmer doesn't car=
e
> which way round labels `__x, __y` bind, providing they're distinct, but t=
he
> typing does care.
>
I've just come across Gaster's 1997 paper 'Polymorphic Extensible Records
for Haskell', which gives a bit more detail on the internals of the
implementation. No surprise: records are stored in a continuous block of
memory, with fields left-to-right by alphabetic order of label. Then the
lacks constraint for each label name is merely an index into the vector,
and gets type-erased. So we could de-arbitrate field selection by taking
them left-to-right. (And introduce the ordering on labels into the formal
typing.)
I see in the Gaster+Jones 1996 paper, there is a possible generic approach:
section 6.2 'First-class labels'. "This increases the expressiveness of our
system quite dramatically, ..." There's to be a distinct kind for labels,
and a type constructor Label :: label -> *. Presumably in 2018 we'd use
kind Symbol for labels. So label `name` is a type variable(?) set to `Label
"name"`. The paper doesn't seem to suggest any of the approach has been
developed, nor can I see evidence of it inside the Hugs code. Specifically
in the code, the parser puts all labels straight into a dedicated symbol
table, where they're treated as constants. (They can only appear in very
clearly identifiable syntactic contexts.) I'm not as sanguine as section
6.2: how to treat label variables as opposed to constants?
* How to treat pattern-matching on two distinct label variables? (example
above)
* How to treat pattern-matching on one label variable appearing in distinct
patterns? Such as
recProject (__x =3D x | rho1) (__x =3D _ | rho2) =3D (__x =3D x | (recProje=
ct rho1
rho2) )
This is currently a valid term, BTW, but is looking for label constant
`__x` in both records.
This is trying to say: if the two records have some label in common (I
don't care which), then take that label and its field; recurse on the
leftovers of the two records. So this will project the LH record on labels
in common with RH record. It's a great design pattern. But worse than the
`recAppend` above, the compiler now has to pick arbitrarily a label that
appears in both arguments; not arbitrarily left-to-right alphabetic
ordering in just one record. (And if that's not possible, don't select that
instance; there's presumably a base case instance for no labels in common.)
It's all fine and dandy using label variables in the formal semantics. It's
quite different supporting them in surface syntax and typing.
> I'd like to write term `( rho1 | rho2 )` to concatenate two records.
> That's currently unrecognised syntax, so I think could be added as such.
> What would be its type/is it principal?
>
> ( rho1 | rho2 ) :: (rho1' \\ rho2') =3D> Rec( rho1' | rho2' ) --
> inventing more syntax
>
> in which constraint `(rho1' \\ rho2')` requires the two rows' labels be
> mutually disjoint -- read "lacks all". Ur/web has something like this.
>
Also Harper&Pierce 1990, 1991 referenced in the G+J paper. We can define
"lacks all" in terms of lacks, by extending the G+J Figure 1 definition of
`\` thusly
* base case: two EmptyRecs lack all labels in common
* recursive case: given two recs that lack all plus some label that both
lack, adding that label at some type to one record, they still both lack
all.
Symbolically:
P ||- {| |} \\ {| |} ;
P ||- r1 \\ r2, r1\l, r2\l
---------------------
P ||- {| l :: tau | r1 |} \\ r2
Note I'm not envisaging `|` as a genuine operator: this is still hard-wired
> syntax; pipe is a reserved symbol in H98 anyway.
>
>
Specifying its formal semantics does need distinguishing one of the
arguments being empty vs not (I'll give the term-level definition as if it
were possible, these need to be in distinct Instances):
(EmptyRec | rho2) =3D rho2
( (__x =3D x | rho1') | rho2) =3D (__x =3D x | (rho1' | rho2) )
Then to achieve full expressivity for a record system, I need just one more
operation: label subtraction or "project away" also known in relational
algebra as "remove" or "project ALL BUT", sometimes symbolised as pi-hat or
pi-overbar. Semantics: given two records with possibly some labels in
common, return the LH argument, with all in-common labels/fields removed.
Note this cunningly avoids requiring the in-common labels to have same
field type, because it ignores the RH argument's fields. The result "lacks
all" attributes of the RH arg.
I think "project away"s semantics can be defined without requiring
pattern-matching on the same label in two different records (and using `=E2=
=8C=86`
to symbolise the operation -- closest I can get to pi-hat):
EmptyRec =E2=8C=86 rho2 =3D EmptyRec
(__x =3D x | rho1') =E2=8C=86 rho2 =3D (__x =3D x | (rho1' =E2=8C=86 rho2))=
, if rho2\__x
(__x =3D x | rho1') =E2=8C=86 rho2 =3D (rho1' =E2=8C=86 rho2), otherwise
Then other generic operations on whole-records can be defined in terms of
the above two, treating records as sets of label-field pairs, and applying
set operations:
rho1 `recIntersect` rho2 =3D (rho1 =E2=8C=86 (rho1 =E2=8C=86 rho2)) -- =
aka projection
rho1 `recUnion` rho2 =3D Just ((rho1 =E2=8C=86 rho2) | (rho1 =E2=8C=86 (rho=
1 =E2=8C=86 rho2)) | (rho2
=E2=8C=86 rho1))
-- providing (rho1 =E2=8C=86 (rho1 =E2=8C=86 rho2)) =3D=3D (rho2 =E2=8C=86 =
(rho2 =E2=8C=86 rho1))
-- otherwise Nothing
`recUnion` is more familiar as record-level relational Natural Join.
Returns a Maybe record, because the arguments might not be equal on the
field values of the labels in common.
So we have set difference, intersection, union. That must be expressively
complete.
AntC
--00000000000030b6de0579d5729a
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div><div dir=3D"auto">On Thu, 1 Nov 2018 at 12:31 AM, Anthony Clayden =C2=
=A0wrote:</div><br></div><div><div class=3D"gmail_quote"><blockquote class=
=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;padd=
ing-left:1ex"><div dir=3D"auto"><br></div><div dir=3D"auto">Label names in =
Trex are literals; there's no such thing as a label variable. (Which is=
why it's a tad annoying that they start lower case.) Furthermore the s=
ame label name must appear in both terms and types -- in fact labels occupy=
a namespace separate vs terms or types. So Trex is a long way from from ge=
neric record handling like:</div><div dir=3D"auto"><br></div><div dir=3D"au=
to">recAppend :: ( rho'\__x ) =3D> Rec rho' -> Rec ( __x :: a=
) -> Rec ( __x :: a | rho')</div><div dir=3D"auto">recAppend rho ( _=
_x =3D x ) =3D ( __x =3D x | rho )</div><div dir=3D"auto"><br></div><div di=
r=3D"auto">in which I've used double-underscore prefix to signify a lab=
el variable. This is intended to extend a record `rho` with a singleton rec=
ord. If we try appending a record with more than one field, beware that fie=
ld order is arbitrary, so this</div><div dir=3D"auto"><br></div><div dir=3D=
"auto">recAppend rho ( __x =3D x, __y =3D y) =3D ...</div><div dir=3D"auto"=
><br></div><div dir=3D"auto">has no principal type (a familiar difficulty).=
The programmer doesn't care which way round labels `__x, __y` bind, pr=
oviding they're distinct, but the typing does care.</div></blockquote><=
div dir=3D"auto"><br></div><div dir=3D"auto">I've just come across Gast=
er's 1997 paper 'Polymorphic Extensible Records for Haskell', w=
hich gives a bit more detail on the internals of the implementation. No sur=
prise: records are stored in a continuous block of memory, with fields left=
-to-right by alphabetic order of label. Then the lacks constraint for each =
label name is merely an index into the vector, and gets type-erased. So we =
could de-arbitrate field selection by taking them left-to-right. (And intro=
duce the ordering on labels into the formal typing.)</div><div dir=3D"auto"=
><br></div><div dir=3D"auto">I see in the Gaster+Jones 1996 paper, there is=
a possible generic approach: section 6.2 'First-class labels'. &qu=
ot;This increases the expressiveness of our system quite dramatically, ...&=
quot; There's to be a distinct kind for labels, and a type constructor =
Label :: label -> *. Presumably in 2018 we'd use kind Symbol for lab=
els. So label `name` is a type variable(?) set to `Label "name"`.=
The paper doesn't seem to suggest any of the approach has been develop=
ed, nor can I see evidence of it inside the Hugs code. Specifically in the =
code, the parser puts all labels straight into a dedicated symbol table, wh=
ere they're treated as constants. (They can only appear in very clearly=
identifiable syntactic contexts.) I'm not as sanguine as section 6.2: =
how to treat label variables as opposed to constants?</div><div dir=3D"auto=
"><br></div><div dir=3D"auto">* How to treat pattern-matching on two distin=
ct label variables? (example above)</div><div dir=3D"auto">* How to treat p=
attern-matching on one label variable appearing in distinct patterns? Such =
as</div><div dir=3D"auto"><br></div><div dir=3D"auto">recProject (__x =3D x=
| rho1) (__x =3D _ | rho2) =3D (__x =3D x | (recProject rho1 rho2) )</div>=
<div dir=3D"auto"><br></div><div dir=3D"auto">This is currently a valid ter=
m, BTW, but is looking for label constant `__x` in both records.</div><div =
dir=3D"auto"><br></div><div dir=3D"auto">This is trying to say: if the two =
records have some label in common (I don't care which), then take that =
label and its field; recurse on the leftovers of the two records. So this w=
ill project the LH record on labels in common with RH record. It's a gr=
eat design pattern. But worse than the `recAppend` above, the compiler now =
has to pick arbitrarily a label that appears in both arguments; not arbitra=
rily left-to-right alphabetic ordering in just one record. (And if that'=
;s not possible, don't select that instance; there's presumably a b=
ase case instance for no labels in common.)</div><div dir=3D"auto"><br></di=
v><div dir=3D"auto">It's all fine and dandy using label variables in th=
e formal semantics. It's quite different supporting them in surface syn=
tax and typing.</div><div dir=3D"auto"><br></div><div dir=3D"auto"><br></di=
v><blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:=
1px #ccc solid;padding-left:1ex"><div dir=3D"auto"></div><div dir=3D"auto">=
<br></div><div dir=3D"auto">I'd like to write term `( rho1 | rho2 )` to=
concatenate two records. That's currently unrecognised syntax, so I th=
ink could be added as such. What would be its type/is it principal?</div><d=
iv dir=3D"auto"><br></div><div dir=3D"auto">( rho1 | rho2 ) :: (rho1' \=
\ rho2') =3D> Rec( rho1' | rho2' ) =C2=A0 =C2=A0-- inventing=
more syntax</div><div dir=3D"auto"><br></div><div dir=3D"auto">in which co=
nstraint `(rho1' \\ rho2')` requires the two rows' labels be mu=
tually disjoint -- read "lacks all". Ur/web has something like th=
is.</div></blockquote><div dir=3D"auto"><br></div><div dir=3D"auto">Also Ha=
rper&Pierce 1990, 1991 referenced in the G+J paper. We can define "=
;lacks all" in terms of lacks, by extending the G+J Figure 1 definitio=
n of `\` thusly</div><div dir=3D"auto"><br></div><div dir=3D"auto">* base c=
ase: two EmptyRecs lack all labels in common</div><div dir=3D"auto">* recur=
sive case: given two recs that lack all plus some label that both lack, add=
ing that label at some type to one record, they still both lack all.</div><=
div dir=3D"auto"><br></div><div dir=3D"auto">Symbolically:</div><div dir=3D=
"auto"><br></div><div dir=3D"auto">P ||- {| |} \\ {| |} ;</div><div dir=3D"=
auto"><br></div><div dir=3D"auto">P ||- r1 \\ r2, r1\l, r2\l</div><div dir=
=3D"auto">---------------------</div><div dir=3D"auto">P ||- {| l :: tau | =
r1 |} \\ r2</div><div dir=3D"auto"><br></div><blockquote class=3D"gmail_quo=
te" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"=
><div dir=3D"auto"> Note I'm not envisaging `|` as a genuine operator: =
this is still hard-wired syntax; pipe is a reserved symbol in H98 anyway.</=
div><div dir=3D"auto"><br></div><div dir=3D"auto"></div></blockquote><div d=
ir=3D"auto"><br></div><div dir=3D"auto">Specifying its formal semantics doe=
s need distinguishing one of the arguments being empty vs not (I'll giv=
e the term-level definition as if it were possible, these need to be in dis=
tinct Instances):</div><div dir=3D"auto"><br></div><div dir=3D"auto">(Empty=
Rec | rho2) =3D rho2</div><div dir=3D"auto">( (__x =3D x | rho1') | rho=
2) =3D (__x =3D x | (rho1' | rho2) )</div><div dir=3D"auto"><br></div><=
div dir=3D"auto">Then to achieve full expressivity for a record system, I n=
eed just one more operation: label subtraction or "project away" =
also known in relational algebra as "remove" or "project ALL=
BUT", sometimes symbolised as pi-hat or pi-overbar. Semantics: given =
two records with possibly some labels in common, return the LH argument, wi=
th all in-common labels/fields removed. Note this cunningly avoids requirin=
g the in-common labels to have same field type, because it ignores the RH a=
rgument's fields. The result "lacks all" attributes of the RH=
arg.</div><div dir=3D"auto"><br></div><div dir=3D"auto">I think "proj=
ect away"s semantics can be defined without requiring pattern-matching=
on the same label in two different records (and using `<span style=3D"colo=
r:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;ba=
ckground-color:rgb(248,248,248)">=E2=8C=86</span>` to symbolise the operati=
on -- closest I can get to pi-hat):</div><div dir=3D"auto"><br></div><div d=
ir=3D"auto">EmptyRec=C2=A0<span style=3D"color:rgb(0,0,102);font-family:mon=
ospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248=
)">=E2=8C=86</span>=C2=A0rho2 =3D EmptyRec</div><div dir=3D"auto">(__x =3D =
x | rho1')=C2=A0<span style=3D"color:rgb(0,0,102);font-family:monospace=
;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">=E2=
=8C=86</span>=C2=A0rho2 =3D (__x =3D x | (rho1'=C2=A0<span style=3D"col=
or:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;b=
ackground-color:rgb(248,248,248)">=E2=8C=86</span>=C2=A0rho2)), if rho2\__x=
</div><div dir=3D"auto">(__x =3D x | rho1')=C2=A0<span style=3D"color:r=
gb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;backg=
round-color:rgb(248,248,248)">=E2=8C=86</span>=C2=A0rho2 =3D =C2=A0(rho1=
9;=C2=A0<span style=3D"color:rgb(0,0,102);font-family:monospace;font-size:1=
2px;white-space:pre-wrap;background-color:rgb(248,248,248)">=E2=8C=86</span=
>=C2=A0rho2), =C2=A0otherwise<br></div><div dir=3D"auto"><br></div><div dir=
=3D"auto">Then other generic operations on whole-records can be defined in =
terms of the above two, treating records as sets of label-field pairs, and =
applying set operations:</div><div dir=3D"auto"><br></div><div dir=3D"auto"=
>rho1 `recIntersect` rho2 =3D (rho1=C2=A0<span style=3D"color:rgb(0,0,102);=
font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:=
rgb(248,248,248)">=E2=8C=86</span>=C2=A0(rho1=C2=A0<span style=3D"color:rgb=
(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;backgro=
und-color:rgb(248,248,248)">=E2=8C=86</span>=C2=A0rho2)) =C2=A0 =C2=A0 -- a=
ka projection</div><div dir=3D"auto">rho1 `recUnion` rho2 =3D Just ((rho1=
=C2=A0<span style=3D"color:rgb(0,0,102);font-family:monospace;font-size:12p=
x;white-space:pre-wrap;background-color:rgb(248,248,248)">=E2=8C=86</span>=
=C2=A0rho2) | (rho1=C2=A0<span style=3D"color:rgb(0,0,102);font-family:mono=
space;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)=
">=E2=8C=86</span>=C2=A0(rho1=C2=A0<span style=3D"color:rgb(0,0,102);font-f=
amily:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(24=
8,248,248)">=E2=8C=86</span>=C2=A0rho2)) | (rho2=C2=A0<span style=3D"color:=
rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;back=
ground-color:rgb(248,248,248)">=E2=8C=86</span>=C2=A0rho1))</div><div dir=
=3D"auto">-- providing (rho1=C2=A0<span style=3D"color:rgb(0,0,102);font-fa=
mily:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248=
,248,248)">=E2=8C=86</span>=C2=A0(rho1=C2=A0<span style=3D"color:rgb(0,0,10=
2);font-family:monospace;font-size:12px;white-space:pre-wrap;background-col=
or:rgb(248,248,248)">=E2=8C=86</span>=C2=A0rho2)) =3D=3D (rho2=C2=A0<span s=
tyle=3D"color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space=
:pre-wrap;background-color:rgb(248,248,248)">=E2=8C=86</span>=C2=A0(rho2=C2=
=A0<span style=3D"color:rgb(0,0,102);font-family:monospace;font-size:12px;w=
hite-space:pre-wrap;background-color:rgb(248,248,248)">=E2=8C=86</span>=C2=
=A0rho1))</div><div dir=3D"auto">-- otherwise Nothing</div><div dir=3D"auto=
"><br></div><div dir=3D"auto">`recUnion` is more familiar as record-level r=
elational Natural Join. Returns a Maybe record, because the arguments might=
not be equal on the field values of the labels in common.</div><div dir=3D=
"auto"><br></div><div dir=3D"auto">So we have set difference, intersection,=
union. That must be expressively complete.</div><div dir=3D"auto"><br></di=
v><div dir=3D"auto"><br></div><div dir=3D"auto">AntC</div></div></div>
--00000000000030b6de0579d5729a--
--===============5149005072537840277==
Content-Type: text/plain; charset="utf-8"
MIME-Version: 1.0
Content-Transfer-Encoding: base64
Content-Disposition: inline
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=
--===============5149005072537840277==--