[Ur] Ur record types as sets of fields

[Anthony Clayden]

> On 3/11/2017, at 2:06 AM, Adam Chlipala <adamc at csail.mit.edu> wrote:
> 
>> 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!

Thanks Adam.

>   And I don't think a long answer is needed.
> 
I'm curious what the full signature would look like. Here's my guess:

    fun natJoin [ t1' :: {Type} ] [ t1_2 :: {Type} ] [ t2' :: {Type} ]
                    [ t1' ~ t1_2 ] [ t1' ~ t2' ] [ t1_2 ~ t2' ]
                    ( t1 : $( t1' ++ t1_2 ) )  ( t2 : $( t1_2 ++ t2' ) )
                    = ??

And how would I invoke it? With those three `~` constraints, does that need 

    natJoin ! ! ! r1 r2

And can Ur figure out the rest?



>> 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.
> 
> 
AntC