Inefficient elaboration of large monadic block

Stream: lean4

[Aaron Tomb]

I am experimenting with using Lean to represent the computations performed by potentially large programs originally written in other languages. In the process, I've come across what I think is an unnecessary inefficiency in elaborating and doing type class inference for large monadic blocks. I'm wondering whether anyone knows whether a) there's a way to write such things that's more efficient, or b) whether making this more efficient by optimizing Lean itself is likely to be feasible. To be more specific, I've been testing with the following program:

set_option maxRecDepth 10000

def AddALot (x: Nat) : StateM Nat Nat := do
  set x
  modifyGet (λ y => ((), y + x))
  <a few hundred copies of the previous>
    let y <- get
  pure y

#eval StateT.run' (AddALot 2) 0

This is very much an artificial example. Real instances would have different statements. But it serves as an interesting benchmark. With Lean's default recursion depth limit, I first encounter an error about reaching the maximum recursion depth. If I increase it to the limit in the code above, I first get an error from macOS about exceeding the maximum stack depth. If I also increase that, it does successfully terminate, but uses more time and memory than I'd expect it should.

Specifically:

$ lake env time -l lean --profile BigDo.lean
compilation of AddALot took 616ms
elaboration took 1.84s
1026
cumulative profiling times:
    attribute application 0.00641ms
    compilation 622ms
    elaboration 1.84s
    import 45.8ms
    initialization 30.8ms
    interpretation 9.98ms
    linting 46.4ms
    parsing 55.2ms
    type checking 6.83ms
    typeclass inference 712ms
        3.46 real         3.28 user         0.12 sys
           269041664  maximum resident set size
          <snip>
         13268910529  cycles elapsed
           225353728  peak memory footprint

As you can see, elaboration and type class inference take the bulk of the time.

I experimented with this after trying something similar in Coq, but using the itree monad, which is substantially more complex, instead of the state monad. The Coq version, with an even larger number of monadic actions, checks in a fraction of a second.

Does anyone here have thoughts about whether this is likely to be resolvable with a reasonable amount of effort?

[Sebastian Ullrich]

do is a complex elaborator in Lean. From your link I'm assuming you're using neither do nor typeclasses in Coq, I would suggest to do the same in Lean if you have such large programs. You could define your own much simpler do notation on top if desired.

[Aaron Tomb]

True, that library defines its own custom syntax rather than using a generic do. I'm not sure why that hadn't already occurred to me, honestly!