Inductive types in Lean

Common types in Lean (e.g., Bool) are not primitives of the language. They are declared via one of Lean’s main primitives: inductive types

Examples

A boolean type:

inductive Bool where
  | false
  | true

An option type:

-- (α : Type) is like a template parameter
-- (ignore the "universe" u)
inductive Option (α : Type u) where
  | none
  | some (a : α)

A list type:

-- A list is defined as either: 
--  1. the "nil" list, or
--  2. a constructor that works by taking a "head" element α and a so-called
--    "tail" list and concatenates them together.
inductive List (α : Type u) where
  | nil
  | cons (head : α) (tail : List α)

An “either, or” type:

inductive Sum (α β : Type u) where     -- A ⊕ B
  | inl (a : α)
  | inr (b : β)

A tuple type:

structure Prod (α β : Type u) where    -- A × B (a one-constructor inductive)
  fst : α
  snd : β

A “unit” type:

inductive Unit where                   -- (really PUnit, but same idea)
  | unit

The “empty” type:

inductive Empty                        -- ⊥: no constructors, so no values

A caveat: a few types, like Nat and String, get extra special treatment from the compiler and kernel for efficiency, such as machine integers.

Syntax

The inductive syntax is:

inductive Name (parameters) where
  | constructor₁ (fields...)
  | constructor₂ (fields...)

• Each | line is a constructor: a way to build a value of the type.
• A constructor’s fields are the data you have to supply to use it (to build the type).
• Every value of the type is built by one of the constructors, and nothing else is.

If you know Rust, you can think of this as an enum:

enum List<T>     { Nil, Cons(T, Box<List<T>>) }
enum Sum<A, B>   { Inl(A), Inr(B) }

Recall the List definition:

inductive List (α : Type u) where
  | nil
  | cons (head : α) (tail : List α)

This definition is recursive, because one of the things the cons constructor takes is a smaller List α.

So, [1, 2, 3] and 1 :: 2 :: 3 :: [] are shorthand Lean notation for:

List.cons 1 (List.cons 2 (List.cons 3 List.nil))

This notation is ordinary library code too: :: is a one-line infixr for List.cons, while [a, b, c] is a syntax declaration desugared by a macro_rules block that folds the elements into nested List.cons applications ending in List.nil.

Note that each List constructor is a function that produces a list:

List.nil  : List α
List.cons : α → List α → List α

(α : Type u) is a parameter, the element type. This is what makes List Nat and List String to be of different types. u is a universe level¹. Ignore it for now.

References

For cited works, see below 👇👇