Duplicated dbg_trace

Stream: lean4

[Alexandre Rademaker]

In the case below, the dbg_trace will print the message twice during the call to f in the evaluation. I am trying to find the place in https://lean-lang.org/doc/reference/latest/ that explains this behavior, but I couldn't find it. Does anyone know?

def test₁ ( n : Nat) :=
   dbg_trace "teste₁: executed twice"
   let k := 2 * n
   fun z => z + k

#eval
  let f := test₁ 10
  f (f 2)

[Sebastian Ullrich]

Given that dbg_trace embeds a side effect in a pure term, it follows that it has no specified semantics. It is, after all, only for debugging.

[Henrik Böving]

The technical reason it happens is that the compiler simplifies the code by inlining f so you get two calls to test1 which is fine for the reason Sebastian points out

[Robin Arnez]

This will also happen with

def test₁ (n : Nat) :=
   dbg_trace "teste₁: executed twice"
   let k := 2 * n
   fun z => z + k

@[noinline, nospecialize]
def testMe (f : Nat → Nat) := f (f 2)

#eval testMe (test₁ 10)

The real reason for it executing twice is that the compiler will always eta-expand, i.e. you get

#eval testMe (fun x => test₁ 10 x)

after compilation

[Notification Bot]

4 messages were moved here from #lean4 > Kernel error in list index notation by Eric Wieser.

[Henrik Böving]

But this one seems to break at another position in the pipeline? The original problem gets turned into:

[simp] size: 6
      def _eval : Std.Format :=
        let _x.1 := 10;
        let _x.2 := 2;
        let _x.3 := test₁ _x.1 _x.2;
        let _x.4 := test₁ _x.1 _x.3;
        let _x.5 := Nat.reprFast _x.4;
        let _x.6 := Std.Format.text _x.5;
        return _x.6

in the first simplification pass. Your example still looks fine after the first simplification pass:

[simp] size: 5
      def _eval : Std.Format :=
        let _x.1 := 10;
        let _x.2 := test₁ _x.1;
        let _x.3 := testMe _x.2;
        let _x.4 := Nat.reprFast _x.3;
        let _x.5 := Std.Format.text _x.4;
        return _x.5

[Henrik Böving]

Which is to say, I think the phenomenon you are describing is the cause for a different class of programs

[Robin Arnez]

Oh yeah, the real real reason here is that test₁ is a function with two arguments at the IR level - the compiler will always eagerly put variables from the return type into arguments so test₁ _x.1 ends up being a partial application.

[Robin Arnez]

Maybe I'm also misremembering the eta expansion pass? Could be that that only was a pass in the old compiler

[Alexandre Rademaker]

Let me see if I am following the discussion here. The point I was trying to make is that expensive is called twice when I expected it to be called once. If I understood @Henrik Böving comment about "inlining f", the evaluation of let f := test₁ 10 ; f (f 2) got expanded to (test₁ 10) ((test₁ 10) 2). So, perhaps the double evaluation is not due to test₁ returning a lambda, but rather how the let assignment of the return value of test₁ is expanded.

def expensive (k : Nat) :=
  dbg_trace "debug: expensive"
  k * 2

def test₁ ( n : Nat) :=
   let k := expensive n
   fun z => z + k

My concrete case is the one below. I wrote makeRank expecting that the construction of the HashMap would occur only once, not every time the lambda it returns is called. My intention was to hide the concrete HashMap API.

def makeRank (prefList : List α) : α → Nat :=
  let d0 := Std.HashMap.emptyWithCapacity 10000
  let d1 := d0.insertMany $ prefList.zipIdx
  fun cid => d1.get! cid

I modified the code to actually return the HashMap, allowing later functions to query it directly.

def makeRank (prefList : List α) : Std.HashMap α Nat :=
  Std.HashMap.emptyWithCapacity prefList.length
    |>.insertMany prefList.zipIdx

[Alexandre Rademaker]

@Robin Arnez that makes sense! So a partial application doesn't actually execute the computation until the point at which the missing argument is needed. Maybe.. that would mean lazy semantics.

[Henrik Böving]

So a partial application doesn't actually execute the computation until the point at which the missing argument is needed

While it is true that this would require a lazy style approach what you are doing is not as general as this. The compiler just eagerly translates the function into

def makeRank (prefList : List α) : α → Nat :=

  fun cid =>
    let d0 := Std.HashMap.emptyWithCapacity 10000
    let d1 := d0.insertMany $ prefList.zipIdx
    d1.get! cid

right at the beginning and the optimizes.

[Robin Arnez]

It is quite easy to prevent this though, by returning a structure wrapper, e.g. { f : α → Nat // True }

[Alexandre Rademaker]

Thanks @Henrik Böving, clear now.

[Alexandre Rademaker]

@Robin Arnez , how that structure wrapper would fit in the behaviour that @Henrik Böving described?

[Robin Arnez]

Well if you define

def makeRank (prefList : List α) : { f : α → Nat // True } :=
  ...

then the compiler can't turn it into

def makeRank (prefList : List α) : { f : α → Nat // True } :=
  fun cid => ...

roughly speaking

[Henrik Böving]

The compiler would see an additional Struct.Mk around your fun. This blocks the eta transformation that Rob referred to above.

[Henrik Böving]

Its quite the hack though, after all the ABI says trivial structure wrappers have the same representation as the wrapped typed so one could argue that the compiler should behave the same in both circumstances I guess? :/