Re: [Ur] Ur record types as sets of fields

On 11/03/2017 08:22 AM, Anthony Clayden wrote: On 4/11/2017, at 12:57 AM, Adam Chlipala 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'

Re: [Ur] Ur record types as sets of fields

> On 4/11/2017, at 12:57 AM, Adam Chlipala 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} ] >>

Re: [Ur] Ur record types as sets of fields

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' ++

Re: [Ur] Ur record types as sets of fields

> On 3/11/2017, at 2:06 AM, Adam Chlipala 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

Re: [Ur] Ur record types as sets of fields

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

[Ur] Ur record types as sets of fields

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