Lean programming

Stream: lean4

[Gareth Ma]

Hi, I am trying out Lean 4 (since a few hours ago), and I came across this example, which doesn't seem to be in Lean 3. Is there any documentation on this yet? All the Id and things. My limited understanding of functional programming thought that things should be immutable, but here there is a mut keyword, and everything seems to be run in the VM or sth.

def prime_sieve (n : ℕ) : Array ℕ := Id.run do
  let mut primes : Array ℕ := Array.empty
  let mut isp : Array Bool := Array.mkArray (n + 1) true
  for i in [2 : n] do
    if isp[i]! then
      primes ← primes.append #[i]
      for j in [1 : n / i] do
        isp ← isp.modify (i * j) (λ _ => false)
  return primes

#eval (prime_sieve 2000000).toList.sum

[Sebastian Ullrich]

Hi! Functional Programming in Lean has a detailed chapter, with a nice summary at the very end, on this: https://leanprover.github.io/functional_programming_in_lean/monad-transformers/do.html

[Sebastian Ullrich]

@David Thrane Christiansen From a cursory search, I don't think the pattern of injecting Id.run is explicitly described anywhere yet? edit: It is at https://leanprover.github.io/functional_programming_in_lean/monad-transformers/do.html?highlight=Id.run#mutable-variables

[Sebastian Ullrich]

Id simply is the identity monad that lets us use do blocks even for non-monadic code

[Gareth Ma]

Thanks a lot, I will have a look. These will probably help with numerical computations in Lean, especially with other numerical performance improvements

[David Thrane Christiansen]

This is in the chapter that is to be released imminently, but perhaps it should occur in earlier as well :-) Sorry for late follow-up here, been busy.

[David Thrane Christiansen]

Wait, yes, it's in the monad transformer chapter.