[Ur] kind syntax and semantics

[Alexei Golovko]

'#Other' means a _name_ of field, but the (~) checks if two _sets_ of fields have empty intersection.

The right syntax is like:
$ cat ab.ur
fun join [record] [other] [ [Other] ~ record ] (r:$record) (f:other) =
    r ++ { Other = f }

val tst = join {} 1

$ cat ab.urs
val join : record ::: {Type} -> other ::: Type ->  [ [Other] ~ record ] =>
    $record -> other -> $(record ++ [ Other = other ])


23.02.2012, 19:02, "Gergely Buday" <gbuday at gmail.com>:
> Hi,
>
> I am trying to code a simple function that augments a record with an {
> Other : other } field. What am I doing wrong?
>
> $ cat implicit.urs
> val join : record ::: {Type} -> other ::: Type ->  [ #Other ~ record ] =>
>           $record -> other -> $(record ++ [ Other = other ])
>
> $ cat implicit.ur
> fun join [record] [other] [ #Other ~ record ] (r:$record) (f:other) =
> r ++ { Other = f }