Updates to records

[j14159]

Need a way to update or add fields to records, e.g.

let r = {x=1, y=2} in
  {r | z=3}

[danabr]

I think there needs to be a way of distinguishing updating and adding fields to a record. Otherwise, a simple typo is enough for me to create a new type of record, instead of updating an existing one.

Perhaps this problem goes away when type annotations are in place so you can annotate the expression with what type of record you intend to use.

[j14159]

I think there are probably cases where manipulation of the type via updates is what we want but I'm having trouble coming up with cases that aren't completely contrived. We could distinguish between updates vs adds, bad syntax examples:

-- type error changing the type in an update:
let r = {x=1, y=2} in
{r | y=(int_to_float y)}

-- let an explicit add/modify change the type:
let r = {x=1, y=2} in
{r + y=2.0}

Or vice-versa on the type error. That seems like it could be confusing though in the long run. I suspect the least confusing way to address for users is using type annotations so people can restrict/specify the contract they want as you mentioned above.

Thoughts?

[saem]

I think there are a number of things going, that you'd want to keep in mind while coming up with a holistic solution. @j14159 and I talked about this elsewhere, just documenting here so others can see.

1. Updating the values of a record but not changing the type
2. Adding a new field(s) to the record, changing the type, but it still works everywhere else the previous type did (sub-type/non-destructive)
3. Changing the type of a field(s) in a record, such that the record is no longer compatible with the previous record

One, and two are easy enough, nothing destructive really happens, there are no surprises, Liskov is happy, and all is right with the world.

Three is where the trouble starts, IMO. To illustrate, consider "changing" the type of an existing field, what we're really doing is dividing the type (factoring out the old), and then multiplying by the new type (bringing in the new) -- records being fancy product types. My understanding isn't amazing here, but that removal is where dragons lie in type theory.

But we can probably get a bit nuanced about this in order to at least keep things well defined and happy for some cases.

One possibility would be to treat additions of new fields (name: type) as overloading, this will likely require more explicit typing when the typer can't suss things out. But that means that there are no more swaps, and all additions are non-destructive. Additions, should probably be separated from updates (as @danabr pointed out) so you don't accidentally add when you wanted to update, or vice versa -- though you might end up with "upsert" as syntactic sugar.

Which leaves the last case of update, which is an intentional dropping of old information, or a transformation. That should be treated differently as a mapping function that transforms the record as a whole, the mapping function need only reference the parts it cares about, and returning a new incompatible type.

[j14159]

Below I'm using the rough syntax convention of { <an existing record> | [new members...]} for the addition/update/replacement of members and {[<existing members>] | <row variable>} in when describing types.

I think we're getting hung up on the idea of mutation.

foo some_rec = {some_rec | y = 0}

The type of the above is {'a} -> {y: int | 'a} where 'a is the row variable as described at the outset here. Similarly:

bar () =
  let rec_a = {x = 0, y = 2} in  -- {x: int, y: int | 'a}
  {rec_a | y = 3.5}              -- {x: int, y: float | 'a}

Since we have immutable values the third line above is an entirely new value distinct from rec_a.

Now if we were thinking to thread a record through some third-party code, we might want to be able to restrict the addition or replacement of fields, let's say:

foo 'a: int -> int -> {'a} -> {x: int, y: int | 'a}
foo x y existing_rec =
  let with_xy = {existing_rec | x = x, y = y} in
  some_third_party_fun with_xy

If we have the above type annotation capabilities and this type signature for the third party function:

some_third_party_fun 'a: {x: int | 'a} -> {x: int, y: float, z: float | 'a}

We should get a type error because the input 'a to foo does not match the output 'a. Allowing the row variable to be specified in type signatures can give us control over additions and the normal specification of fields controls "modifications".

Modification syntax is borrowed from Elm and type syntax roughly from Objects and Aspects: Row Polymorphism. Perhaps we want to unify the syntax for consistency where the row variable and existing record value always come first, e.g.

foo 'a: {'a} int -> {'a | x: int}
foo some_rec x = {some_rec | x = x}