Last updated 2024-03-03
Lean is starting to look like a great option for functional programming. It has been heavily adopted by the mathematics community but no so much by the Functional Programming community. This means that there is not yet much library support day to application development, but the bones of the language look really nice for FP.
Its a pure FP language with monadic effects, do
notation, typeclasses, and dependent types, quotient types, a powerful
macro system, a C FFI, and from what I understand it is
very fast.
At this point I wouldn't recommend it for production work outside of theorem proving, but given some time that could change.
In my own personal interest I have created this minimal guide for Haskell developers learning Lean. This article is not at all intended to replace any of the much more substantial documentation generated by the Lean community (and listed at the end of this article). Rather, this is just a quick FAQ for common questions a Haskell developer will have when starting to learn Lean. Contributions would be greatly appreciated here.
Elan is Lean's
equivalent to GHCUp. It automatically puts lean and lake files in your
build path. Versions can be pinned via the lean-toolchain
file.
Elan is recommended even on Nixos systems and seems to integrate fairly well.
Lake is the standard build system. You can initialize a new project with:
mkdir hello
cd hello
lake init helloDependencies and build targets are managed via
lakefile.lean.
Note, most of these examples were taken from Functional Programming in Lean which is a much more complete introduction to the language.
You can drop the #eval meta command anywhere in your
code:
#eval 1 + 2
This can be triggered via LSP mode or the lean compiler directly.
Terms are defined using the def keyword:
def hello := "Hello"
The type of a term can be ascribed:
def lean : String := "Lean"
The basic way to define functions is by adding parameters (with or
without ascriptions) to a def statement:
def add1 (n : Nat) : Nat := n + 1
Lambdas are
Because types are first class, we can define type aliases as ordinary terms:
def Str : Type := String
def aStr : Str := "This is a string."
structure Point where
x : Float
y : Float
deriving Repr
def origin : Point := { x := 0.0, y := 0.0 }
Both are declared with the inductive keyword:
inductive List (α : Type u) where
| nil : List α
| cons (head : α) (tail : List α) : List α
inductive Bool where
| false : Bool
| true : Bool
GADTs can also be done using inductive statements.
data Expr a where
Lit :: Int -> Expr Int
Str :: String -> Expr String
Add :: Expr Int -> Expr Int -> Expr IntBecomes:
inductive Expr : Type → Type
| lit : Int → Expr Int
| str : String → Expr String
| add : Expr Int → Expr Int → Expr Int
Lean distinguishes between "normal" and "index" parameters. Normal
parameters must always be given first. Once an index parameter is
introduced, all subsequent paremeters are assumed to be indices as well.
This means we have to put the nat index on a Vec after the
α param:
inductive Vec : Type u → Nat → Type u where
| vnil : Vec α 0
| vcons (head : α) (tail : Vec α n) : Vec α (Nat.succ n)
More details found here.
case statements are called match
statments:
def isZero (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => false
structure PPoint (α : Type) where
x : α
y : α
deriving Repr
Lean is a dependently typed language which means it has Sigma and Pi types. Explaining what that means is out of the scope of this FAQ. Here is a more detailed article.
For reference here is their syntax to build a dependent pair
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
Lean has loogle which does not appear work as well as Hoogle but I think that is inevitable given that dependent types can require computation during typechecking.
Lean has Monads!
Lean is a pure functional language with monadic effects and
do notation:
do a ← s,
b ← t,
f a b,
return (g a b)
Lean has a very similar typeclass hierarchy in the prelude:
Note that some common classes need to be found in
Mathlib. Classes requiring proofs are noted.
Foldable has been folded into
Traversable.Profunctor but should be recoverable using CategoryTheory.Functor
from Mathlib (requires proofs).Aeson style typeclasses can be found in mathlib:
To my knowledge nothing exists yet.
Lean uses a non-monadic recursive descent parser: https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Basic.html
To my knowledge no parser generator or parser combinator libraries exist yet.
To my knowledge nothing exists yet.
This stuff is all mixed togther in the following modules: