The Lean track is now live on Exercism!
Lean is both a general-purpose functional programming language and a theorem prover.
Its syntax is heavily influenced by Haskell, and it includes many of its characteristics, for example:
- An expressive type system.
- Pure functions by default, with stateful functions isolated.
- Immutable data structures with efficient sharing of common structure.
- Efficient recursion.
On top of that, Lean also supports many distinct features. A few of them include:
- Dependent types - Types can depend on values, even runtime values not known at compile time.
- Propositions as types - In Lean, logical propositions are types, and proofs are values of those types.
- Integrated proof assistant - Lean has a powerful proof assistant capable of validating complex proofs.
Together, these characteristics allow specifications and constraints to be encoded directly into types. To construct a value of such a type, you must prove it satisfies the required constraints. The proof becomes part of the value itself, making invalid states effectively unrepresentable and the program’s logic mathematically sound.
Lean also combines its strong type system with practical performance features, such as:
-
Efficient in-place updates of unshared data - Lean keeps track of references to values and, if a value is not shared, updates are performed destructively (i.e., no new copy is created). This allows efficient implementations of data structures such as arrays.
-
Imperative constructs in impure code - Some algorithms are more naturally implemented using imperative constructs such as
for,while, and explicit mutation. Lean supports this in impure (monadic) code.
Ready to explore the power of dependent types and theorem proving? Give it a try!