← All papers
'do' unchained: embracing local imperativity in a purely functional language (functional pearl)
cs.LO
Aug 19, 2022 · v1
TL;DR
Describes Lean 4's do-notation extensions that compile imperative patterns via monad transformers.
Abstract
Monadic programming in pure functional languages has long provided a disciplined way to incorporate effects. This paper presents a system of extended do-notation for the Lean 4 programming language that allows users to write local mutable variables, early return, loops with break/continue, and other imperative patterns directly inside pure functional code, compiling them away via monad transformers without runtime overhead.
Problem
Monadic programming in pure functional languages provides disciplined effects, but writing imperative-style code (mutable variables, early return, loops with break/continue) requires verbose monad transformer boilerplate that obscures intent.
Approach
The paper presents extended do-notation for Lean 4 that allows users to write local mutable variables, early return, loops with break/continue, and other imperative patterns directly inside pure functional code. These constructs compile away via monad transformers without runtime overhead.
Results
The system enables imperative patterns to be written naturally inside pure functional Lean 4 code while maintaining purity guarantees, with the compiler eliminating all overhead from the monad transformer encoding.