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

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.

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