Loops in Lean programming language

Question

I'm starting to learn about Lean programming language https://leanprover.github.io

I've found out that there are functions, structures, if/else, and other common programming commands.

However, I haven't found anything to deal with loops. Is there a way of iterating or repeating a block of code in Lean? Something similar to for or while in other languages. If so, please add the syntaxis or an example.

Thank you in advance.

Answer 1

Like other functional programming languages, loops in Lean are primarily done via recursion. For example:

-- lean 3
def numbers : ℕ → list ℕ
| 0 := []
| (n+1) := n :: numbers n

This is a bit of a change of mindset if you aren't used to it. See: Haskell from C: Where are the for Loops?

To complicate matters, Lean makes a distinction between general recursion and structural recursion. The above example is using structural recursion on ℕ, so we know that it always halts. Non-halting programs can lead to inconsistency in a DTT-based theorem prover like lean, so it has to be strictly controlled. You can opt in to general recursion using the meta keyword:

-- lean 3
meta def foo : ℕ → ℕ
| n := if n = 100 then 0 else foo (n + 1) + 1

---

In lean 4, the do block syntax includes a for command, which can be used to write for loops in a more imperative style. Note that they are still represented as tail-recursive functions under the hood, and there are some typeclasses powering the desugaring. (Also you need the partial keyword instead of meta to do general recursion in lean 4.)

-- lean 4
partial def foo (n : Nat) : Nat :=
  if n = 100 then 0 else foo (n + 1) + 1

def mySum (n : Nat) : Nat := Id.run do
  let mut acc := 0
  for i in [0:n] do
    acc := acc + i
  pure acc