One-field structures in Lean code

Stream: lean4

[Denis Gorbachev]

There are some one-field structures in Lean code (see examples below). IIRC, creating an element of a new one-field structure is an unnecessary allocation. Is there a reason to do this, instead of just using the type of that field?

Examples:

structure FilePath where
  toString : String

structure MessageLog where
  msgs : PersistentArray Message := {}

structure String.Pos where
  byteIdx : Nat := 0

Could be just

def FilePath := String

def MessageLog := PersistentArray Message

def String.Pos := Nat

(default values could be provided by Zero instances)

[Damiano Testa]

docs#Polynomial is another example. In this case, I think that one of the main motivation for cutting the DefEq was that there were continuous "leaks" and the implementation sometimes surfaced where it was undesirable.

[Scott Morrison]

The compiler is smart enough to optimize these away.

[Shreyas Srinivas]

Denis Gorbachev said:

There are some one-field structures in Lean code (see examples below). IIRC, creating an element of a new one-field structure is an unnecessary allocation. Is there a reason to do this, instead of just using the type of that field?

Examples:

structure FilePath where
  toString : String

structure MessageLog where
  msgs : PersistentArray Message := {}

structure String.Pos where
  byteIdx : Nat := 0

Could be just

def FilePath := String

def MessageLog := PersistentArray Message

def String.Pos := Nat

(default values could be provided by Zero instances)

If you use them in proofs, I recommend using abbrev instead of def

[Mac Malone]

Denis Gorbachev said:

Is there a reason to do this, instead of just using the type of that field?

Yes, a structure wrapper prevents Lean from automatically coercing between the wrapper type and the wrapped type (i.e., using a Nat where a String.Pos is expected or vice versa works without error with a def but produces a type error with a structure wrapper).

[Denis Gorbachev]

Thank you for answers!