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