Lean 3 structure extension quiz

Stream: general

[Kyle Miller]

Here's a little quiz: how many times does "hey!" print when you evaluate foo?

structure A :=
(x : ℕ)
(y : ℕ)

structure B extends A :=
(z : ℕ)

def foo (a : A) : B := {z := 3, ..trace "hey!" a}
-- or equivalently {trace "hey!" a with z := 3}

#eval foo ⟨1,2⟩

[Alex J. Best]

Twice? I think that makes sense if trace "hey" a is substituted everywhere a would be

[Kyle Miller]

Yes, it's twice (though if the CSE pass applied here it should only be once). That said, the type of B.mk is A → ℕ → B so one could imagine the structure notation to be smarter about it.

The Lean 4 equivalent, in comparison, only prints "hey!" once.

structure A where
  x : Nat
  y : Nat
  deriving Repr

structure B extends A where
  z : Nat
  deriving Repr

def foo (a : A) : B := {Id.run do dbg_trace "hey!" pure a with z := 3}

#eval foo ⟨1, 2⟩

(do #print foo to see why)

[Kyle Miller]

I'm wondering if there's any performance impact in Lean 3 due to this when there are typeclass instances created with complicated .. expressions.