Confused about thunks

Stream: lean4

[James Sully]

Hi there, my use of thunks doesn't seem to be thunking:

def sum : List Nat → Nat := List.foldl Nat.add 0

def main (args : List String) : IO Unit := do
  let expensive : Thunk Nat := Thunk.mk fun () ↦ sum (List.range 100000000)
  match args with
  | [] => IO.println "Skipping expensive computation"
  | _ => IO.println s!"Result: {expensive.get}"

$ time ./.lake/build/bin/laziness
Skipping expensive computation

________________________________________________________
Executed in    1.94 secs    fish           external
   usr time    1.10 secs  898.00 micros    1.10 secs
   sys time    0.84 secs  131.00 micros    0.84 secs

$ time ./.lake/build/bin/laziness asdf
Result: 4999999950000000

________________________________________________________
Executed in    1.93 secs    fish           external
   usr time    1.05 secs  724.00 micros    1.05 secs
   sys time    0.87 secs  105.00 micros    0.87 secs

It seems to take the same amount of time either way. What am I doing wrong here?

[Sebastian Ullrich]

Make the computation dependent on args so that the compiler can't hoist it out

[James Sully]

Thanks! Seems like a bit of a footgun

[James Gallicchio]

it definitely is, for anyone trying to time code: https://leanprover.zulipchat.com/#narrow/streams/public/search/.22set_option.20compiler.2Eextract_closed.20false.22
but I'm not entirely sure what the "right" approach here is