[Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/02/2017 09:51 PM, Anthony Clayden wrote:
> 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' ) )
>                      = ??

One possibility is:
     t1 ++ (t2 --- t1_2)
It's not clear to me what result type you expect, though.

> And how would I invoke it? With those three `~` constraints, does that need
>
>      natJoin ! ! ! r1 r2
>
> And can Ur figure out the rest?

Disjointness proofs are implicit by default, so just
     natJoin r1 r2