notation for unpacking structures and field assignment

Stream: lean4

[Tomas Skrivan]

I'm missing some convenience notation for working with structures in imperative code.

Field assignment: you can't assign fields with s.fst := 1 for s : ℕ×ℕ.

#eval Id.run do
  let mut s := (1,2)
  s.fst := 3 -- error
  s

This is fixable with a simple macro

open Lean Parser
syntax atomic(Term.ident) noWs "." noWs ident ":=" term : doElem

macro_rules
| `(doElem| $s:ident . $a:ident := $x) => `(doElem| $s:ident := {$s with $a:ident := $x})

now you can write

#eval Id.run do
  let mut s := (1,2)
  s . fst := 3
  s

Unfortunately, there has to be a space round the dot, s . fst not s.fst. How can I fix this?

---

Unpacking structures: I would like to unpack structure s : ℕ×ℕ and then refer to its field s.fst and s.snd only with fst and snd.

#eval
  let ⟨..⟩ := (1,2)
  fst -- error

doable with a simple elaborator

syntax (name:=let_struct_syntax) withPosition("let" "⟨..⟩" ":=" term) optSemicolon(term) : term

open Lean Elab Term Syntax Meta
elab_rules (kind:=let_struct_syntax) : term
| `(let ⟨..⟩ := $x:term
    $b) => do

  let X ← inferType (← elabTerm x none)
  let .const struct _ := X.getAppFn' | throwError "structure expected"
  let info := getStructureInfo (← getEnv) struct
  let ids := info.fieldNames.map (fun n => mkIdent n)
  let stx ← `(let ⟨$ids,*⟩ := $x; $b)
  elabTerm stx none

Now the above works but it does not work in do block. Ideally I would like to do

#eval Id.run do
  let mut ⟨..⟩ := (1,2)
  fst := 3
  (fst,snd) -- (3,2)

However I do not know how to do this as you can't write elaborator for doElem syntax category. Ideally it is only a macro but I need to infer the type of $x and look it up for the field names.

---

Packing structures: once you unpack a structure you most likely need to pack it again. Any tips what the notation should look like?

These are the two options I can think of but I do not like either of them.

#eval Id.run do
  let mut ⟨..⟩ := (1,2)
  fst := 3
  pack Prod

#eval Id.run do
  let mut s ⟨..⟩ := (1,2)
  fst := 3
  pack s

[Tomas Skrivan]

In the process of writing the question I was able to solve the field assignment

syntax (name:=do_field_assigment) (priority:=high) atomic(Term.ident) ":=" term : doElem

macro_rules (kind:=do_field_assigment)
| `(doElem| $s:ident := $x) => do
  let .str (.str .anonymous s) a := s.getId
    | `(Parser.Term.doReassign| $s:ident := $x)
  let s := mkIdent (.mkSimple s)
  let a := mkIdent (.mkSimple a)
  let stx ← `(Parser.Term.doReassign| $s:ident := {$s with $a:ident := $x} )
  dbg_trace (prettyPrint stx)
  return stx

#check Id.run do
  let mut s := (1,2)
  s.fst := 3
  s

This prevents you from having let variables with dot in their name, but is that really a common thing to do?

[Kyle Miller]

You sort of beat me to it, but here's another way:

macro_rules
| `(doElem| $x:ident := $val) => do
  let .str n f := x.getId | Macro.throwUnsupported
  if n == .anonymous then Macro.throwUnsupported
  let o := mkIdentFrom x n
  let field := mkIdentFrom x (Name.mkSimple f)
  `(doElem| $o:ident := {$o with $field:ident := $val})

#eval Id.run do
  let mut s := (1,2)
  s.fst := 3
  s

[Kyle Miller]

I didn't know let variables with dots in names was even supported.

[Tomas Skrivan]

Kyle Miller said:

(I didn't know let variables with dots in names was even supported.)

(I didn't test it but assumed so ... testing ... yes they are supported :)

[Tomas Skrivan]

Nice! I didn't realize that I don't have to define a new syntax. I had to explicitly mention Parser.Term.doReassignto prevent an infinite loop.

[Kyle Miller]

There's some issue with the unused variable linter still, but at least it seems to be functional.

[Kyle Miller]

Tomas Skrivan said:

Unpacking structures

An issue with this idea is that it could shadow other variable names. At least with

#eval
  let {..} := (1,2)
  0

(which fails) you can see that fst and snd are in the local context with hygienic names, so the feature is sort of there.

I'd hesitate to make a rule like ".. creates non-hygienic names if it is not shadowing other names in the context" since that could lead to really confusing bugs when you copy/paste code. For example, if you add an argument to a function you could cause .. to not add a name. Or, if .. always shadowed names, that would open you up to bugs from adding a field to a structure.

[Tomas Skrivan]

I agree that it is potentially problematic but recently I wrote this code

Id.run do
  let mut state := state
  state.s := - (state.invH * state.g)
  state.g_previous := state.g
  state.dx := state.alpha • state.s
  state.x_previous := state.x
  state.x := state.s + state.x
  state.f_x_previous := state.f_x

  return state

and I feel that this would be cleaner

Id.run do
  let mut ⟨..⟩ := state
  s := - (invH * g)
  g_previous := g
  dx := alpha • s
  x_previous := x
  x := s + x
  f_x_previous := f_x

  return (pack state)

[Tomas Skrivan]

In in scenarios like this I think it is reasonable to do this.

[Kyle Miller]

Maybe you could make an elaborator pack MyStruct that finds the names of all the fields and expands to { field1, field2, field3 }, and then you could write let mut (pack MyStruct) := state and end with return pack MyStruct?

[Kyle Miller]

This is using the principle of "the pattern should use the same syntax as the constructor"

[Tomas Skrivan]

Good idea! I will try that

[Mauricio Collares]

Arguably related: there was an old mathlib4 PR experimenting with lenses at mathlib4#290