what is [computed_field] attribute

Stream: lean4

[Asei Inoue]

I have read the definition of Lean.Name.

inductive Name where
  /-- The "anonymous" name. -/
  | anonymous : Name
  /--
  A string name. The name `Lean.Meta.run` is represented at
  ```lean
  .str (.str (.str .anonymous "Lean") "Meta") "run"
  ```
  -/
  | str (pre : Name) (str : String)
  /--
  A numerical name. This kind of name is used, for example, to create hierarchical names for
  free variables and metavariables. The identifier `_uniq.231` is represented as
  ```lean
  .num (.str .anonymous "_uniq") 231
  ```
  -/
  | num (pre : Name) (i : Nat)
with
  /-- A hash function for names, which is stored inside the name itself as a
  computed field. -/
  @[computed_field] hash : Name → UInt64
    | .anonymous => .ofNatCore 1723 (by decide)
    | .str p s => mixHash p.hash s.hash
    | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))

what does [computed_field] attribute mean?

• what is the main benefit of this attribute?
• how different from having Name.hash function separately?

[Mario Carneiro]

A computed field is like a regular function from the perspective of the theory, but the data layout of the type includes the values of computed fields, so that they are O(1) to calculate. This is an important optimization for Name and Expr so that they can have fast hashing

[Asei Inoue]

@Mario Carneiro Thanks.

Interesting feature. I would like to try it myself.
why this raise an error?

set_option autoImplicit false
set_option relaxedAutoImplicit false

inductive MyList (α : Type) where
  | nil : MyList α
  | cons (a : α) (xs : MyList α) : MyList α
with
  -- unexpected token '('; expected ':'
  @[computed_field] length {α : Type} : MyList α → Nat
  | .nil => 0
  | .cons _ xs => 1 + length xs

[Mario Carneiro]

I think the parameters of the inductive are already in scope

[Asei Inoue]

set_option autoImplicit false
set_option relaxedAutoImplicit false

inductive MyList (α : Type) where
  | nil : MyList α
  | cons (a : α) (xs : MyList α) : MyList α
with
  -- unknown identifier 'α'
  @[computed_field] length : MyList α → Nat
  | .nil => 0
  | .cons _ xs => 1 + length xs

[Mario Carneiro]

looks like several bugs are involved here. Warning that @[computed_field] is not a particularly polished feature, and it has extremely few (no?) uses in the wild beyond the ones for Name and Expr. This works:

inductive MyList (α : Type) where
  | nil : MyList α
  | cons (a : α) (xs : MyList α) : MyList α
with
  @[computed_field] length : ∀ α, MyList α → Nat
  | _, .nil => 0
  | _, .cons _ xs => 1 + length _ xs

[Asei Inoue]

Should I open an issue?

[Kim Morrison]

It seems rather low priority? Perhaps for now don't treat this as a publicly available feature, and instead an internal optimization hack.

[Kyle Miller]

I can't substantiate this, but I seem to remember that computed_field should be regarded as being just for Expr. It lets us write Expr using Lean rather than needing it to be written in C++.