[Ur] Ur record types as sets of fields
Adam Chlipala
adamc at csail.mit.edu
Thu Nov 2 09:06:52 EDT 2017
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.
More information about the Ur
mailing list