[Ur] Ur record types as sets of fields

[Anthony Clayden]

Hi citizens of Ur,

A long while back, Adam responded in a discussion about Ur's record system http://blog.ezyang.com/2012/04/how-urweb-records-work-and-what-it-might-mean-for-haskell/#comment-3705

I'm wondering whether Ur's disjointness constraint might be used to build a record merge operator -- as needed for Relational Algebra Natural Join.

(I'm finding it a bit weird using `~` for disjointness: I'm so used to it being a type equality constraint in Haskell. So apologies if I stuff up. Also in the Ur materials I looked at, I don't see how to express type equality? For equality of record types I mean same set of field names, and same type of each corresponding field.)

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?

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(?)

Thank you
AntC

[Adam Chlipala]

Post by Anthony Clayden
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
t1' -- fields private to t1
t1_2 -- fields in common
t2' -- fields private to t2
t1 is [ t1' ++ t1_2 ];
t2 is [ t1_2 ++ t2' ];
the result of Natural Join is [ t1' ++ t1_2 ++ t2' ].
[ 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.

Post by Anthony Clayden
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.

[Anthony Clayden]

Post by Adam Chlipala

Post by Anthony Clayden
I'm wondering whether Ur's disjointness constraint might be used to build a record merge operator -- as needed for Relational Algebra Natural Join.
t1' -- fields private to t1
t1_2 -- fields in common
t2' -- fields private to t2
t1 is [ t1' ++ t1_2 ];
t2 is [ t1_2 ++ t2' ];
the result of Natural Join is [ t1' ++ t1_2 ++ t2' ].
[ 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.

Post by Adam Chlipala
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?

Post by Adam Chlipala

Post by Anthony Clayden
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

[Adam Chlipala]

Post by Anthony Clayden
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.

Post by Anthony Clayden
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

[Anthony Clayden]

Post by Adam Chlipala

Post by Anthony Clayden
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' ) )
= ??

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.

Post by Adam Chlipala
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.

Post by Adam Chlipala

Post by Anthony Clayden
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

[Adam Chlipala]

Post by Anthony Clayden

Post by Adam Chlipala

Post by Anthony Clayden
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' ) )
= ??

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.

Post by Adam Chlipala
It's not clear to me what result type you expect, though.

Oh, that was in the earlier message: [ t1' ++ t1_2 ++ t2' ]

Oh, you meant the brackets to signify a list, Haskell-style?  But then
the argument types don't make sense, as they only give single records,
not lists or sets of records.

In real Ur/Web code, such a function would be a bad smell, since SQL
queries do all this natively.