Update assignment syntax

[Kha]

Compared to languages that allow mutable references for this/self/..., updating a mutable variable with the result of one of its "methods" is still a bit verbose in Lean:

references := references.insert ref v

It would be great to have a shorthand that avoids repeating the variable name, but I can't really think of a great syntax.

references :=.insert ref v
references.=insert ref v

The former syntax could also be generalized to any trailing term syntax, perhaps depending on lack of whitespace

i :=+ 1

Looks a little weird though...

Any favorite bikeshed colors?

[Kha]

I've been thinking about this while doing Advent of Code in Lean, and coincidentally saw this thread today: https://old.reddit.com/r/ProgrammingLanguages/comments/rleiot/an_idea_for_a_operator/

[gebner]

Any favorite bikeshed colors?

I prefer colors that can be layered on top of each other and can be painted on many different surfaces.

So it would be nice if the same syntax was used for do-assignments, structure updates, and maybe also let-bindings.

It would also be nice if you could update in structure fields, array indices, list indices, hashmap entries, etc. And in combination, and extensible.

As a concrete proposal:

references %= (·.push 42)   -- notation copied without thinking or endorsement from Haskell's lenses
ctx.references %= (·.push 42)   -- more complicated lvalues
ctx.references[7] %= (· + 1)
let ctx.references[7] %= (· + 3)   -- why not let-bindings as well?
monadState.references[8] := 1 -- compiles to something equivalent to modify fun st => let st.references[8] := 1; st

The %= do-elem should probably support a do-elem rhs as well.

EDIT: operators like += or :=. can of course then be defined on top of these as macros.

[Kha]

Yeah, I was bothered by the parentheses in my mind, but it doesn't look too bad that way. This is also $= in Idris' structure notation, but I suppose we now avoid this meaning of $.

[vvs-]

FWIW, I recall that jq has |= for update assignment.

[tydeu]

monadState.references[8] := 1 -- compiles to something equivalent to modify fun st => let st.references[8] := 1; st

Two suggestions for monadState: using the this keyword: this.references[8] := 1 or a starting .: .references[8] := 1).

[Kha]

Since I think the first example is still the vastly most prevalent use case, and reusing existing keywords, even while slightly bending them, is usually better than introducing new token soup, one more suggestion that just popped into my mind:

mut references.insert ref v

[tydeu]

@Kha combining your suggestion with @gebner's your original example we would have something like:

mut (·.push 42) references 
mut (·.push 42) ctx.references 
mut (· + 1) ctx.references[7] 
let mut (· + 3) ctx.references[7]  --- ???
mut 1 monadState.references[8] 

While this could work, I am not a fan of the putting the function before the variable and I think the lack of an equality operator (and its variable-left, value-right ordering) makes it much harder for new users. to adopt the syntax. I guess some of that could be papered over, though, by convenience macros for special cases (e.g., for +=, -=, :=.push, etc.).

[Kha]

Correct, my suggestion should absolutely not be combined with Gabriel's :)

[tydeu]

This is also $= in Idris' structure notation, but I suppose we now avoid this meaning of $. FWIW, I recall that jq has |= for update assignment.

Another suggestion for the operator (in @gebner's example) is |>= since that is Lean's equivalent mixture of the application operator and assignment. That is, x |>= f applies f to x (like x |> f) and then assigns it to x.

[gebner]

For reference, this is a working version of my proposal:

import Lean
open Lean Macro

declare_syntax_cat lvalue

/--
`lvalue ←% x => action` applies `action` to `lvalue`.
In the local context of `action`, the variable `x` will be bound to the
previous value of the `lvalue`.  The `action` should return the updated value.
-/
syntax lvalue "←%" ident "=>" doElem : doElem

/-- `lvalue %= func` modifies `lvalue` using `func` -/
macro a:lvalue "%=" f:term : doElem =>
  `(doElem| $a:lvalue ←% x => pure <| $f:term x)

/-- `lvalue += off` increases `lvalue` by `off` -/
macro a:lvalue "+=" b:term : doElem =>
  `(doElem| $a:lvalue %= fun x => x + $b)

syntax ident : lvalue
macro_rules
  | `(doElem| $n:ident ←% $x:ident => $act:doElem) =>
    `(doElem| $n:ident ← do let $x := $n:ident; $act:doElem)

#eval Id.run do
  let mut x := 1
  let mut y := 10
  x ←% it => do y := 0; pure (it + 2)
  return x + y

syntax lvalue "." ident : lvalue
macro_rules
  | `(doElem| $n:ident ←% $x:ident => $act:doElem) => do
    let Syntax.ident (val := Name.str a@(Name.str ..) b ..) .. := n
      | Macro.throwUnsupported
    `(doElem| $(mkIdentFrom n a):ident.$(mkIdentFrom n b):ident ←% $x:ident => $act:doElem)
macro_rules
  | `(doElem| $a:lvalue . $b:ident ←% $x:ident => $act:doElem) =>
    `(doElem| $a:lvalue ←% aval => do
      let $x:ident := aval.$b:ident
      let $b:ident ← $act:doElem
      pure { aval with $b:ident })

#eval Id.run do
  let mut x := (1,2)
  x.fst %= (· + 1)
  x.fst += 2
  pure x

syntax lvalue noWs "[" term "]" : lvalue
macro_rules
  | `(doElem| $a:lvalue[$i] ←% $x:ident => $act:doElem) =>
    `(doElem| $a:lvalue ←% aval => do
      let $x:ident := (aval).getOp $i
      let $x:ident ← $act:doElem
      pure <| (aval).modifyOp $i fun _ => $x:ident)

#eval Id.run do
  let mut x := (#[1,2,3], 42)
  x.fst[1] += 100
  pure x

-- monadState can't be a fake keyword because then monadState.fst doesn't work
macro_rules
  | `(doElem| monadState ←% $x:ident => $act:doElem) => do
    `(doElem| do
      let $x:ident ← get
      let $x:ident ← $act:doElem
      set $x:ident)

#eval Id.run do StateT.run (s := (42, 100)) do
  monadState.fst += 10
  pure 100

syntax "(" lvalue ")" : lvalue
macro_rules
  | `(doElem| ($lval:lvalue) ←% $x:ident => $act:doElem) =>
    `(doElem| $lval:lvalue ←% $x:ident => $act:doElem)

syntax "let" ident : lvalue
macro_rules
  | `(doElem| let $a:ident ←% $x:ident => $act:doElem) =>
    `(doElem| do
      let mut a := $a:ident
      a ←% $x:ident => $act:doElem
      let $a:ident := a)

#eval Id.run do
  let x := 42
  let x += 10
  pure x

[tydeu]

EDIT: @gebner, you literally posted your example while I was spell-checking mine. 🤣

So, I went ahead an coded up a quick demonstration of @gebner's original idea mixed with mine. Here is the code:

import Lean.Parser.Term

open Lean Parser

syntax thisState := "this"

macro (priority := high) thisState " := " val:term : doElem =>
  `(doElem| set $val)

syntax thisField := "this:" noWs ident

macro field:thisField " := " val:term : doElem =>
  `(doElem| modify (fun s => {s with $(field[2]):ident := $val}))

--

syntax reassignable :=
  thisField <|> thisState <|> ident

syntax reassignable " |>= " term : doElem

macro_rules
| `(doElem| this |>= $fn) =>
  `(doElem| modify $fn)
| `(doElem| this:$field |>= $fn) =>
  `(doElem| modify (fun s => {s with $field:ident := $fn s.$field}))
| `(doElem| $var:ident |>= $fn) =>
  `(doElem| $var:ident := $fn $var)

---

macro var:reassignable " :=." noWs meth:ident args:Term.argument* : doElem =>
  `(doElem| $var:reassignable |>= (·.$meth $args*))

macro var:reassignable " ++= " val:term : doElem =>
  `(doElem| $var:reassignable |>= (· ++ $val))

--

structure Foo where
  str : String
  num : Nat

def test2 := Id.run do
  discard <| Id.run <| flip StateT.run "abc" do
    this ++= "xyz"
    -- note that `.<ident>` notation already gives us this for free
    this |>=.map (·.toUpper)
    this |>=.toLower
    this := "hi"
    pure ()
  discard <|Id.run <| flip StateT.run (⟨"abc", 0⟩  : Foo) do
    let mut arr := #[]
    arr ++= #[2, 3]
    -- extra notation is need here though because the expected type is not known
    arr :=.push 5
    this:str ++= "cde"
    this := (⟨"hi", 2⟩ : Foo)
    pure ()

I personally quite like how it turned out. What does everyone else think?

[nomeata]

If we ever get to this, maybe there is a variant where array setting could look like

do
  a[i] := x

or similarly slick.