<div><div dir="auto">On Thu, 1 Nov 2018 at 12:31 AM, Anthony Clayden  wrote:</div><br></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><br></div><div dir="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 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:</div><div dir="auto"><br></div><div dir="auto">recAppend :: ( rho'\__x ) => Rec rho' -> Rec ( __x :: a) -> Rec ( __x :: a | rho')</div><div dir="auto">recAppend rho ( __x = x ) = ( __x = x | rho )</div><div dir="auto"><br></div><div dir="auto">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</div><div dir="auto"><br></div><div dir="auto">recAppend rho ( __x = x, __y = y) = ...</div><div dir="auto"><br></div><div dir="auto">has no principal type (a familiar difficulty). The programmer doesn't care which way round labels `__x, __y` bind, providing they're distinct, but the typing does care.</div></blockquote><div dir="auto"><br></div><div dir="auto">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.)</div><div dir="auto"><br></div><div dir="auto">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?</div><div dir="auto"><br></div><div dir="auto">* How to treat pattern-matching on two distinct label variables? (example above)</div><div dir="auto">* How to treat pattern-matching on one label variable appearing in distinct patterns? Such as</div><div dir="auto"><br></div><div dir="auto">recProject (__x = x | rho1) (__x = _ | rho2) = (__x = x | (recProject rho1 rho2) )</div><div dir="auto"><br></div><div dir="auto">This is currently a valid term, BTW, but is looking for label constant `__x` in both records.</div><div dir="auto"><br></div><div dir="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 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.)</div><div dir="auto"><br></div><div dir="auto">It's all fine and dandy using label variables in the formal semantics. It's quite different supporting them in surface syntax and typing.</div><div dir="auto"><br></div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"></div><div dir="auto"><br></div><div dir="auto">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?</div><div dir="auto"><br></div><div dir="auto">( rho1 | rho2 ) :: (rho1' \\ rho2') => Rec( rho1' | rho2' )    -- inventing more syntax</div><div dir="auto"><br></div><div dir="auto">in which constraint `(rho1' \\ rho2')` requires the two rows' labels be mutually disjoint -- read "lacks all". Ur/web has something like this.</div></blockquote><div dir="auto"><br></div><div dir="auto">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</div><div dir="auto"><br></div><div dir="auto">* base case: two EmptyRecs lack all labels in common</div><div dir="auto">* 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.</div><div dir="auto"><br></div><div dir="auto">Symbolically:</div><div dir="auto"><br></div><div dir="auto">P ||- {| |} \\ {| |} ;</div><div dir="auto"><br></div><div dir="auto">P ||- r1 \\ r2, r1\l, r2\l</div><div dir="auto">---------------------</div><div dir="auto">P ||- {| l :: tau | r1 |} \\ r2</div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="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="auto"><br></div><div dir="auto"></div></blockquote><div dir="auto"><br></div><div dir="auto">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):</div><div dir="auto"><br></div><div dir="auto">(EmptyRec | rho2) = rho2</div><div dir="auto">( (__x = x | rho1') | rho2) = (__x = x | (rho1' | rho2) )</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">I think "project away"s semantics can be defined without requiring pattern-matching on the same label in two different records (and using `<span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span>` to symbolise the operation -- closest I can get to pi-hat):</div><div dir="auto"><br></div><div dir="auto">EmptyRec <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2 = EmptyRec</div><div dir="auto">(__x = x | rho1') <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2 = (__x = x | (rho1' <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2)), if rho2\__x</div><div dir="auto">(__x = x | rho1') <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2 =  (rho1' <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2),  otherwise<br></div><div dir="auto"><br></div><div dir="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="auto"><br></div><div dir="auto">rho1 `recIntersect` rho2 = (rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> (rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2))     -- aka projection</div><div dir="auto">rho1 `recUnion` rho2 = Just ((rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2) | (rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> (rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2)) | (rho2 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho1))</div><div dir="auto">-- providing (rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> (rho1 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho2)) == (rho2 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> (rho2 <span style="color:rgb(0,0,102);font-family:monospace;font-size:12px;white-space:pre-wrap;background-color:rgb(248,248,248)">⌆</span> rho1))</div><div dir="auto">-- otherwise Nothing</div><div dir="auto"><br></div><div dir="auto">`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.</div><div dir="auto"><br></div><div dir="auto">So we have set difference, intersection, union. That must be expressively complete.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">AntC</div></div></div>