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.
_______________________________________________
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
