[Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/01/2017 08:26 PM, Anthony Clayden wrote:
> I'm wondering whether Ur's disjointness constraint might be used to 
> build a record merge operator -- as needed for Relational Algebra 
> Natural Join.
>
> Given two records of type t1, t2 with (some) fields in common, some 
> private; let's chop their fields into projections:
> t1' -- fields private to t1
> t1_2 -- fields in common
> t2' -- fields private to t2
>
> Then we can say (treating `++` as union of fields):
> t1 is [ t1' ++ t1_2 ];
> t2 is [ t1_2 ++ t2' ];
> the result of Natural Join is [ t1' ++ t1_2 ++ t2' ].
>
> We also require those projections to be disjoint:
> [ t1' ~ t1_2 ], [ t1' ~ t2' ], [ t1_2 ~ t2' ]
>
> Those constraints uniquely 'fix' all those record types modulo 
> ordering of names/fields in the records. Is that going to work?

Short answer: yes, it works!  And I don't think a long answer is needed.

> It also feels weird using `++` for record union: again it strongly 
> suggests Haskell's list concatenation, which is non-commutative. 
> Perhaps Ur's `++` is non-commutative(?) It's the inbuilt semantics for 
> `$( )`, `!` that make `++` commutative in effect(?)

Yes, Ur/Web [++] is commutative.  I'm not sure what constitutes an 
"explanation of why," but yours seems reasonable.