tail-call optimisation

Stream: general

[Kevin Kappelmann]

Is Lean supporting tail-call optimisation?

[Neil Strickland]

This thread is relevant. I would summarise it as saying that Mario's approach persuades Lean to do the optimisation, but it does need persuasion. But I am not an expert on these things, and others might disagree with that summary.

[Edward Ayers]

See also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tail-call.20elimination.3F

[Edward Ayers]

I think the short answer is no because I would expect a TCO to optimise rev_aux.

set_option trace.compiler.code_gen true
def rev_aux {α : Type} : list α → list α → list α
|acc [] := acc
|acc (h::t) := rev_aux (h :: acc) t

outputs

[compiler.code_gen]  rev_aux._main._meta_aux 3
0: push 0
1: builtin_cases list.cases_on, 2 4
2: push 1
3: goto 11
4: push 4
5: push 3
6: push 1
7: cnstr #1 2
8: scnstr #0
9: ginvoke rev_aux._main._meta_aux
10: drop 2
11: ret
[compiler.code_gen]  rev_aux 1
0: scnstr #0
1: closure rev_aux._main 1
2: ret

If I'm not mistaken TCO would replace step 9 with a goto 1 and also some register shuffling. I could also be misinterpreting what is going on here.

[Kevin Kappelmann]

If I'm not mistaken TCO would replace step 9 with a goto 1 and also some register shuffling. I could also be misinterpreting what is going on here.

I'd say so too, but then again, we could both be wrong :')