Handling of record field names is inconsistent: different for record creation and record update

[lukaszcz]

In record creation, e.g.,

let r1 := A in
mkR@{r1 := r1}

the r1 on the right side refers recursively to the field being defined.

In record update, e.g.,

let r1 := A in
r@R{r1 := r1}

the r1 on the right side refers to the r1 defined by the let.

Complete example:

module rec;

type T := A | B;

type R := mkR { rt : T };

r : R := mkR@{ rt := A };

g : T -> T
  | A := B
  | B := A;

f : R -> R
  | r@mkR@{rt} := (r@R{rt := g rt});

main : T := R.rt (f r);

This type-checks and prints B.

We should somehow unify the behaviour.

Possible solutions

1. Make references in record update recursive by default. I don't like this one, because it's making life harder for the users.
2. Make zero-argument functions in record creation/update always non-recursive and "proper" functions with multiple args recursive. This seems to match most closely with actual use-cases. In virtually all cases when using a zero-argument name in record creation you don't want it to be recursive. In most cases when you define a proper function you want it to be recursive by default.
3. Have a different way of indicating that a field defined in record creation/update is recursive: some rec keyword or something like this.

Option 1 seems to make the language most "unified" (the syntax for definitions is everywhere the same), but also most annoying to use the record update/creation.

Options 2, 3 make the syntax less consistent than 1, but seem to align more closely with actual use-cases.

Any more options?

[lukaszcz]

In general, maybe we should re-think how we handle local recursive definitions and invent some rules that align with actual use-cases but are still not too complex to be confusing.

Because when someone writes e.g.,

let x := x + 1 in ..

they don't want x to be defined recursively by this equation.

I think it's quite annoying and confusing that we treat zero-argument function definitions as recursive by default. Maybe a general exception is reasonable here?

But then we need some way of indicating that we want a recursive definition. In an eager language this is extremely rare for zero-argument definitions, but one could want something like:

let rec x := c (\{z := if | z == 0 := d | else := x})

I think all zero-argument recursive definitions need the terminating annotation anyway. There are no arguments that could decrease, so they always fail the termination checker.

[lukaszcz]

I propose the following general rule. A definition is treated as recursive only if one of the following holds:

• it has at least one argument on the left, e.g., f (a : Nat) : Nat := ...,
• it has a clause with at least one pattern, e.g.,

f : Nat -> Nat
  | a := ...

• it has no arguments and only one zero-pattern clause, but the body is a lambda-abstraction, e.g.,

f : Nat -> Nat := \{a := ...}

Otherwise, the definition is not recursive.

We treat all definitions this way (top-level, let, record creation/update). I think this aligns quite closely with actual use-cases and is not too complex to be obscure.

In a let, we could allow a rec keyword to override this behaviour and indicate that a definitions should be recursive. This will be used extremely rarely and is only for completeness. We don't need to reserve rec as a general keyword - check for it only in let.

Perhaps we might even do without the rec keyword and in the very rare cases when one needs a recursive zero-argument definition simulate it with a dummy argument:

let x' (dummy : Unit) : C := c (\{z := if | z == 0 := d | else := x' dummy});
    x : C := x' unit

[lukaszcz]

This is super-confusing: the inconsistency is also with record puns.

The expression

let r2 := 3 in
mkR@{r1 := r2; r2}

is equivalent to

mkR 3 3

The expression

let r2 := 3 in
mkR@{r1 := r2; r2 := 4}

is equivalent to

mkR 4 4

In the first expression, the r2 on the right is bound by the let, in the second it's bound in the mutually-recursive definition of record fields.

[janmasrovira]

Summary of what we briefly discussed online

1. When defining a term we should only bind the name being defined in the body if the definition looks like a function. This needs to be consistent across top definition, record creation/update, let definition. Looking like a function means that either there is at least an argument on the left of the :, or there is at least one guard. This is what @lukaszcz proposed in the first two points. We don't need rec for now and most likely we won't need it in the future.
2. For record updates, we would access the old value by prefixing the reference by @. I.e.

   let x := 3 in
   r@R{ x := @x + 1; -- `@x` refers to the value of the field `x` in `r` before the update. 
        y := x}      -- `x` refers to the `x` defined in the outside let. 
   

3. Record puns do not need to change for record creation. They need to be supported for record updates (Allow punning in record updates #2967).

[lukaszcz]

Idea: should we use .x instead of @x to refer to the old value in the record update? I think we're overusing @ and .x seems intuitive: you're qualifying a variable with an implicit scope of the record update.

[lukaszcz]

We agreed to not have a special syntax to refer to the old value, for now.