> On 4/11/2017, at 12:57 AM, Adam Chlipala <[email protected]> wrote: > >> 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)
IIUC that's merely projecting away the t1_2 attributes from t2; then cross-multiplying with t1(?) What it needs is matching records type t1 with records type t2 that have the same values in the fields in common -- i.e. in their t1_2 fields. That's typically implemented as a record-by-record fold over one argument. > It's not clear to me what result type you expect, though. > Oh, that was in the earlier message: [ t1' ++ t1_2 ++ t2' ] Perhaps that should be $( t1' ++ t1_2 ++ t2' ) What I gave was based on the `fun proj ...` definition in the 'Ur by example' section of your paper, which doesn't give the type of the result. >> 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 > cool. thanks AntC _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
