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

A Shape can 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.53975
12#eval area (Shape.rectangle 3.0 4.0) -- 12.0
13#eval area (Shape.triangle 6.0 4.0)  -- 12.0

❗

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.

Open vs Closed Keyword

Use open to avoid repeating the type name:

lean

1inductive Color where
2  | red | green | blue
3  deriving Repr
4
5-- Without open
6def withoutOpen : Color := Color.red
7
8-- With open  
9open Color in
10def withOpen : Color := red
11
12-- Open for a block
13open Color
14def c1 : Color := red
15def c2 : Color := blue

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:

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

Structures Next: Recursive Data