SOLOMON'S BLOG

functional programming, permaculture, math

**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 hello
```

Dependencies 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.

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⟩
```

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.

- Mathlib.Control.Bifunctor.Bifunctor
- Init.Control.Basic.MonadControl (MonadBaseControl)
- Mathlib.Algebra.Group.Defs.Semigroup (requires proof)
- Mathlib.Algebra.Group.Defs.Monoid (requires proof)
- Mathlib.Control.Traversable.Basic.Traversable
- Mathlib.CategoryTheory.Category.Basic.Category (requires proofs)

Notably Absent

`Foldable`

has been folded into`Traversable`

.`Profunctor`

but should be recoverable using CategoryTheory.Functor from`Mathlib`

(requires proofs).

- Unit
- Init.Prelude.List
- Init.Control.Id (Identity)
- Init.Control.Reader
- Init.System.IO
- Init.Control.State
- Init.Control.Option (Maybe)
- Init.Prelude.Except (Either)
- Init.Core.Sum
- Std.Data.HashMap.Basic.HashMap
- Init.Prelude.Array
- Init.Prelude.String Init.Data.String.Basic Init.Data.String.Extra

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

- IO.Mutex Similar to an IO Ref.
- IO.Promise
- Init.Data.Channel

ST/STM