Module 2 · Lesson 1

Products (Structures)

Structures bundle multiple values together into a single type. They're similar to structs in Rust/C or records in other functional languages.

Defining Structures

Use the structure keyword to define a new data type with named fields:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Create instances
6def origin : Point := { x := 0.0, y := 0.0 }
7def p1 : Point := { x := 3.0, y := 4.0 }
8
9-- Access fields with dot notation
10#eval p1.x  -- 3.0
11#eval p1.y  -- 4.0

The where keyword introduces the field list. Each field has a name and a type.

Anonymous Constructor Syntax

For concise construction, use angle brackets ⟨...⟩ (type\langle and \rangle, or just use ASCII<...>):

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Anonymous constructor (order matters!)
6def p1 : Point := ⟨3.0, 4.0⟩
7
8-- ASCII alternative
9def p2 : Point := Point.mk 3.0 4.0
10
11-- Both are equivalent to:
12def p3 : Point := { x := 3.0, y := 4.0 }

ℹ

With anonymous constructors, field order matters. Named field syntax { x := ..., y := ... } is clearer for structures with many fields.

Default Field Values

Fields can have default values, making them optional during construction:

lean

1structure Config where
2  host : String := "localhost"
3  port : Nat := 8080
4  debug : Bool := false
5
6-- Use all defaults
7def defaultConfig : Config := {}
8
9-- Override some fields
10def prodConfig : Config := { port := 443, debug := false }
11
12-- Override all
13def customConfig : Config := { host := "api.example.com", port := 9000, debug := true }
14
15#eval defaultConfig.host  -- "localhost"
16#eval prodConfig.port     -- 443

Deriving Common Functionality

Use deriving to automatically generate useful instances:

lean

1structure Person where
2  name : String
3  age : Nat
4  deriving Repr, DecidableEq, Inhabited
5
6def alice : Person := { name := "Alice", age := 30 }
7def bob : Person := { name := "Bob", age := 25 }
8
9-- Repr allows #eval to print the structure
10#eval alice  -- { name := "Alice", age := 30 }
11
12-- DecidableEq allows equality comparison
13#eval alice == bob   -- false
14#eval alice == alice -- true
15
16-- Inhabited provides a default value
17#eval (default : Person)  -- { name := "", age := 0 }

Key Takeaway

deriving Repr is essential for debugging—it makes your structures printable with #eval.

Updating Structures

Structures are immutable, but you can create modified copies with "update" syntax:

lean

1structure Person where
2  name : String
3  age : Nat
4  deriving Repr
5
6def alice : Person := { name := "Alice", age := 30 }
7
8-- Create a new Person with updated age
9def olderAlice : Person := { alice with age := 31 }
10
11-- Original is unchanged
12#eval alice.age      -- 30
13#eval olderAlice.age -- 31

Accessor Functions

You can create small helper functions to keep structure access clean and reusable.

lean

1structure User where
2  name : String
3  score : Nat
4  deriving Repr
5
6def isTopUser (u : User) : Bool := u.score >= 100
7def displayName (u : User) : String := s!"@{u.name}"
8
9#eval isTopUser { name := "alice", score := 120 }  -- true
10#eval displayName { name := "bob", score := 10 }

Functions on Structures

Define functions that work with your structures:

lean

1structure Point where
2  x : Float
3  y : Float
4  deriving Repr
5
6def Point.distance (p1 p2 : Point) : Float :=
7  let dx := p2.x - p1.x
8  let dy := p2.y - p1.y
9  Float.sqrt (dx * dx + dy * dy)
10
11def origin : Point := ⟨0.0, 0.0⟩
12def p : Point := ⟨3.0, 4.0⟩
13
14#eval Point.distance origin p  -- 5.0
15#eval origin.distance p        -- 5.0 (method syntax!)

Notice the method syntax: origin.distance p. When a function is in the Point namespace and takes a Point as its first argument, you can call it with dot notation.

Nested Structures

Structures can contain other structures:

lean

1structure Address where
2  street : String
3  city : String
4  deriving Repr
5
6structure Person where
7  name : String
8  address : Address
9  deriving Repr
10
11def alice : Person := {
12  name := "Alice"
13  address := { street := "123 Main St", city := "Boston" }
14}
15
16#eval alice.address.city  -- "Boston"
17
18-- Nested update
19def movedAlice : Person := {
20  alice with
21  address := { alice.address with city := "Cambridge" }
22}

Deep Dive: Structures vs Classes

Lean also has a class keyword, but it's for type classes (covered later), not OOP-style classes. Structures are the primary way to bundle data.

There is no inheritance in the OOP sense. Composition (nesting structures) is the preferred pattern.

Exercise: Update a Record

Create a function that increments a person's age and returns the updated record.

lean

1structure Person where
2  name : String
3  age : Nat
4
5def birthday (p : Person) : Person :=
6  { p with age := p.age + 1 }
7
8#eval birthday { name := "Eve", age := 29 }

Pattern Matching on Structures

You can destructure structures in function parameters:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Destructure in the parameter list
6def magnitude : Point → Float
7  | ⟨x, y⟩ => Float.sqrt (x * x + y * y)
8
9-- Or use a match expression
10def magnitude' (p : Point) : Float :=
11  match p with
12  | ⟨x, y⟩ => Float.sqrt (x * x + y * y)
13
14-- Or just use field access
15def magnitude'' (p : Point) : Float :=
16  Float.sqrt (p.x * p.x + p.y * p.y)
17
18#eval magnitude ⟨3.0, 4.0⟩  -- 5.0

Local Scope Next: Inductive Types