Module 2 · Lesson 2

Sums (Inductive Types)

Inductive types let you define data that can be one of several variants—like enums with data. This is the foundation of functional domain modeling.

Basic Inductive Types

An inductive type lists all possible forms a value can take:

lean

1inductive Weekday where
2  | sunday
3  | monday
4  | tuesday
5  | wednesday
6  | thursday
7  | friday
8  | saturday
9  deriving Repr
10
11def today : Weekday := Weekday.wednesday
12
13#eval today  -- Weekday.wednesday

Each variant (called a "constructor") is a possible value of the type. This is similar to enums in other languages.

Inductive Types with Data

Unlike simple enums, constructors can carry data:

lean

1inductive Shape where
2  | circle (radius : Float)
3  | rectangle (width : Float) (height : Float)
4  | triangle (base : Float) (height : Float)
5  deriving Repr
6
7def myCircle : Shape := Shape.circle 5.0
8def myRect : Shape := Shape.rectangle 3.0 4.0
9
10#eval myCircle  -- Shape.circle 5.000000

A Shapecan be a circle with a radius, a rectangle with dimensions, or a triangle. This is called a "sum type" because a value is one of the options.

Key Takeaway

Sum types model exclusive choices. A Shape is a circle OR a rectangle OR a triangle—never multiple at once. This makes impossible states unrepresentable.

Pattern Matching on Inductives

To use inductive types, you pattern match on their constructors:

lean

1inductive Shape where
2  | circle (radius : Float)
3  | rectangle (width : Float) (height : Float)
4  | triangle (base : Float) (height : Float)
5
6def area : Shape → Float
7  | Shape.circle r => 3.14159 * r * r
8  | Shape.rectangle w h => w * h
9  | Shape.triangle b h => 0.5 * b * h
10
11#eval area (Shape.circle 5.0)        -- 78.539750
12#eval area (Shape.rectangle 3.0 4.0) -- 12.000000
13#eval area (Shape.triangle 6.0 4.0)  -- 12.000000

❗

Lean requires you to handle ALL cases. If you forget one, your code won't compile. This exhaustiveness checking prevents entire classes of bugs.

The Option Type

Option is a built-in inductive type for values that might not exist:

lean

1-- Option is defined roughly as:
2-- inductive Option (α : Type) where
3--   | none : Option α
4--   | some : α → Option α
5
6def safeDivide (x y : Nat) : Option Nat :=
7  if y == 0 then none else some (x / y)
8
9#eval safeDivide 10 2   -- some 5
10#eval safeDivide 10 0   -- none
11
12-- Pattern match to extract the value
13def divideOrZero (x y : Nat) : Nat :=
14  match safeDivide x y with
15  | none => 0
16  | some result => result

Modeling Real Domains

Inductive types excel at representing complex domain logic:

lean

1inductive PaymentMethod where
2  | cash
3  | creditCard (number : String) (expiry : String)
4  | bankTransfer (accountId : String)
5  deriving Repr
6
7inductive OrderStatus where
8  | pending
9  | paid (method : PaymentMethod)
10  | shipped (trackingId : String)
11  | delivered
12  | cancelled (reason : String)
13  deriving Repr
14
15-- Create realistic orders
16def order1 : OrderStatus := OrderStatus.pending
17def order2 : OrderStatus := OrderStatus.paid (PaymentMethod.creditCard "1234..." "12/25")
18def order3 : OrderStatus := OrderStatus.cancelled "Customer request"

Notice how the type system prevents invalid states: you can't have a tracking ID without the order being shipped, and you can't have a payment method without the order being paid.

Three Ways to Shorten Constructor Names

Writing Shape.rectangle everywhere gets old. There are three ways out, in increasing order of preference:

lean

1inductive Color where
2  | red | green | blue
3  deriving Repr
4
5-- 1. Fully qualified — always works, always unambiguous
6def c0 : Color := Color.red
7
8-- 2. open, for one declaration or for the rest of the section
9open Color in
10def c1 : Color := red
11
12open Color
13def c2 : Color := blue
14
15-- 3. Leading-dot notation: Lean fills in the namespace from the EXPECTED type.
16--    No import, no open, no ambiguity — this is the idiomatic choice.
17def c3 : Color := .green
18
19def isWarm : Color → Bool
20  | .red   => true
21  | .green => false
22  | .blue  => false
23
24#eval isWarm .red   -- true

💡

Prefer the leading dot. open Color pulls red, green, and blue into scope for the whole file, which collides the moment you define a second colour-like type. .red is resolved from the type Lean already expects, so it can never be ambiguous.

Deep Dive: Inductive vs Structure

Structures are for products: combining multiple pieces of data together (AND). A Point has an x AND a y.

Inductive types are for sums: representing alternatives (OR). A Shape is a circle OR a rectangle.

Both can be combined: a constructor in an inductive type can hold multiple fields (product inside sum), and a structure field can be an inductive type (sum inside product).

Generic Inductive Types

Inductive types can be parameterized over other types. This lets you build reusable containers and wrappers that work with any element type.

lean

1-- A result that's either a success value or an error message
2inductive Result (α : Type) where
3  | ok (value : α)
4  | error (message : String)
5  deriving Repr
6
7def parseInt (s : String) : Result Nat :=
8  match s.toNat? with
9  | some n => Result.ok n
10  | none => Result.error s!"'{s}' is not a valid number"
11
12#eval parseInt "42"    -- Result.ok 42
13#eval parseInt "hello" -- Result.error "'hello' is not a valid number"

Boolean Logic with Inductives

Even Bool is an inductive type:

lean

1-- Bool is defined as:
2-- inductive Bool where
3--   | false : Bool
4--   | true : Bool
5
6-- Implement our own not
7def myNot : Bool → Bool
8  | true => false
9  | false => true
10
11-- Implement and
12def myAnd : Bool → Bool → Bool
13  | true, true => true
14  | _, _ => false
15
16#eval myNot true         -- false
17#eval myAnd true false   -- false

What Lean Generates For You

An inductive declaration is not just a type — it silently adds a family of definitions and theorems to the environment. Knowing they exist explains a lot of what tactics do later.

lean

1inductive Shape where
2  | circle (radius : Float)
3  | rectangle (width : Float) (height : Float)
4
5-- The recursor: "to build something for every Shape, handle every constructor"
6#check @Shape.rec
7-- {motive : Shape → Sort u} →
8--   ((radius : Float) → motive (Shape.circle radius)) →
9--   ((width height : Float) → motive (Shape.rectangle width height)) →
10--   (t : Shape) → motive t
11
12-- Injectivity: constructors never lose information
13#check Shape.circle.injEq
14-- (Shape.circle r₁ = Shape.circle r₂) = (r₁ = r₂)
15
16-- Disjointness: different constructors are never equal
17#check Shape.noConfusion

ℹ

These two facts — constructors are injective and disjoint — are what make pattern matching sound, and what the cases, injection, and simp tactics use under the hood. When simp reduces circle r = rectangle w hto False, it is using noConfusion. Every match you write is compiled down to Shape.rec.

Useful deriving Clauses

lean

1inductive Color where
2  | red | green | blue
3  deriving Repr, DecidableEq, Inhabited, BEq, Hashable, Ord
4
5#eval Color.red                    -- Color.red        (Repr)
6#eval Color.red == Color.blue      -- false            (BEq)
7#eval (default : Color)            -- Color.red        (Inhabited: the FIRST constructor)
8#eval compare Color.red Color.blue -- Ordering.lt      (Ord: declaration order)
9
10-- DecidableEq is stronger than BEq: it lets you decide equality PROPOSITIONS
11example : Color.red ≠ Color.blue := by decide

⚠

deriving Inhabited picks the first constructor that Lean can build, and deriving Ord orders by declaration order. Both are silent decisions that your code may come to depend on — if the order matters, write the instance by hand rather than relying on where you happened to put a constructor.

The Built-in Sum Type

When you want "an A or a B" without inventing names, Lean has Sum, written ⊕. It is the generic version of every two-constructor type you would otherwise write by hand.

lean

1-- inductive Sum (α β : Type) where
2--   | inl (a : α) : Sum α β
3--   | inr (b : β) : Sum α β
4
5#check (Nat ⊕ String)                -- Type
6#eval  (Sum.inl 3 : Nat ⊕ String)    -- Sum.inl 3
7
8def render : Nat ⊕ String → String
9  | .inl n => s!"number {n}"
10  | .inr s => s!"text {s}"
11
12#eval render (.inr "hi")   -- "text hi"

💡

Prefer a named type over ⊕ in your own domain code. Result with ok/error reads far better than Nat ⊕ String, and the constructor names document which side means what. ⊕ earns its place in generic library code, where there is nothing meaningful to name.

Exercise: Describe a Shape

Write a function that turns a Shape into a short description.

lean

1inductive Shape where
2  | circle (radius : Float)
3  | rectangle (width : Float) (height : Float)
4  | triangle (base : Float) (height : Float)
5
6def describe : Shape → String
7  | Shape.circle r => s!"circle r={r}"
8  | Shape.rectangle w h => s!"rectangle {w}x{h}"
9  | Shape.triangle b h => s!"triangle {b}x{h}"
10
11#eval describe (Shape.circle 2.5)

Structures Next: Recursive Data