SOLOMON'S BLOG
functional programming, permaculture, math

Lean For Haskell Developers

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.

Installer

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.

Build System

Lake is the standard build system. You can initialize a new project with:

mkdir hello
cd hello
lake init hello

Dependencies and build targets are managed via lakefile.lean.

Basic Syntax

Note, most of these examples were taken from Functional Programming in Lean which is a much more complete introduction to the language.

eval

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.

Functions

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

Type Aliases

Because types are first class, we can define type aliases as ordinary terms:

def Str : Type := String
def aStr : Str := "This is a string."

Record Types

structure Point where
  x : Float
  y : Float
deriving Repr

def origin : Point := { x := 0.0, y := 0.0 }

Recursive and Sum Types

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 Int

Becomes:

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.

Pattern Matching

case statements are called match statments:

def isZero (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => false

Polymorphism

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

Sigma and Pi?

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⟩

Hoogle?

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.

Effects? IO

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)

Functor/Applicative/Monad/Traversable etc?

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.

Notably Absent

Common Types

Common Tools/Libaries

JSON Serialization

Aeson style typeclasses can be found in mathlib:

Web Servers/Clients/TLS/JOSE/JWT

To my knowledge nothing exists yet.

Parsing

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.

Database Clients

To my knowledge nothing exists yet.

File Handling, FilePaths, Directories, and Environment

This stuff is all mixed togther in the following modules:

IORefs/Mutation/Concurrency

ST/STM

Package Registry?

Where can I learn more?