Record updater

[jldodds]

It would be convenient to have a record update expression, such as Haskell's:

> let foo = Foo { a = 1, b = 2, c = "Hello" }         -- create a Foo
> let updateFoo x = x { c = "Goodbye" }               -- function to update Foos
> updateFoo foo                                       -- update the Foo
Foo {a = 1, b = 2, c = "Goodbye" }

[brianhuffman]

The syntax would have to be a bit different from Haskell, since x {c = "Goodbye"} would be ambiguous: Is this updating a record field of x, or applying function x to an argument of type {c : String}?

Perhaps something like x {c := "Goodbye"} would work.

[elliottt]

You could also do something like { x with c = "Goodbye" }, like in ocaml and f#.

[weaversa]

I like Trevor's syntax best so far.

[yav]

What type would you like this to have? A monomorphic update would be fairly easy, I think:

set l :: Has l a t => a -> t -> t

However, an update function that allows for changing the type of the filed would be tricky to do.

[jldodds]

My needs are met by monomorphic update. I don't think it's unreasonable to ask the user to write their own function for an update that changes field types, since they probably won't do that too often.

[brianhuffman]

In a discussion with @robdockins a while back, another concern came up: nested record updates. We might like to have nice syntax for updating, say, field x of the nested record r = {u = 0, v = {x = 3, y = 4}}. With the Haskell-style proposals above, this would require mentioning r multiple times, like r { v := r.v { x := 9 } }.

[yav]

@jldodds @brianhuffman @robdockins @elliottt

I was thinking a bit about the Cryptol records this morning, and I'd like to
propose the following design. We start by adding a new language construct
for updating records---this is a construct in the same way selectors have
special entry in the AST. Also, like selectors, we only accept expressions
where the types resolve fully (i.e., Has never appears in schemas).
The new construct has the following type rule:

r : t,  f : a -> a,  Has l r a
------------------------------
    { r | l -> f } : t

In the typing rule r is something with a notion of a filed (e.g., a record), l is a label, f is a function that maps the old value of a field to the new one.

In addition, we add a bunch of syntactic sugar to make writing updates nicer:

1. Setting a field:

{ r | x = e }  ~> { r | x -> \_ -> e }

2. Updating multiple fields:

{ r | x -> f, y -> g } ~> { { r | x -> f } | y -> g }

3. Updater functions:

{ _ | x -> f } ~> \s -> { s | x -> f }

4. Nested updates:

{ r | x.y -> f } ~> { r | x -> { _ | y -> f }}

I tried this syntax with our parser and it works OK, as long as the r is a simple expression (i.e., no applications). We could also allow arbitrary expressions, but then we get shift-reduce conflicts, which are benign, I think, so we could allow those too probably.

I think this should cover the basics. Furthermore, here are some examples that I think should work and are more exotic:

1. Updating a tuple t: { t | 0 = 42 }. Is it weird that the syntax looks like a record? We've been talking about unifying those anyway...

2. Consider a sequence of records: ps : [2] { x : Bool, y : [8] }. We support "lifted" selectors, so ps.x : [2] Bool. The same sort of thing should work in updates:

{ ps | x = [ True, False ] } ~> [ {r | x = v } | r <- ps | v <- [True,False] ] 

3. We also allow lifting through functions: f : [64] -> { x : Bool, y : [8] }, we allow f.x to be a function of type [64] -> Bool. Symmetrically, we should be able to update values like f:

{f | x = g } ~> \i -> { f i | x = g i }

Clearly the last two are a bit odd, but they don't look hard to implement, and I think that having the consistent behavior is nice.

Most of the desugaring should probably happen in the front end, just like the desugaring for projection. So in the back end, we'd just need to implement the ordinary update on records and pairs, so I don't think there should be a big burden on the evaluation/reasoning system.

Also, I wrote everything with ~> as the primitive, but everything also works with = being primitive instead, which may be simpler for reasoning purposes?

{ r | x -> f } ~> { r | x = f r.x }

[yav]

After thinking about this some more, here are some more notes:

1. It may be nicer if updating a field takes an expression with a free variable for the old value of a field, instead of an explicit function. This would allow us to write things like { r | x -> x + 1 }, instead of { r | x -> \x -> x + 1 }

2. With nested updates, the order in which the updates are done might matter. For example, consider { r | x = a, x.y = b }. The above definitions specify a strict order, so technically this is not a problem, but in practice it may lead to subtle errors, so we may want to give a warning if there are overlapping updates. Alternatively, we could just treat that as an error.

[brianhuffman]

@yav is this feature done? We should close this ticket once documentation and test cases are in place.

[yav]

I think so, there might even be documentation, but I should probably add some tests. I've assigned it to myself.