Algebraic Data Types

Structures and Inductive Types

• A structure is a product type: every value carries all of its named fields simultaneously
• Construct a structure with { field := value, ... }; access a field with s.field
• { s with field := newVal } creates a copy with one field changed, leaving the rest untouched
• deriving Repr lets #eval print values; deriving BEq enables ==
• An inductive type is a sum type: a value is exactly one of its named constructors
• Constructors can carry data; a constructor with no arguments behaves like an enum variant
• match expr with | Ctor args => body pattern-matches on a value; Lean rejects incomplete matches at compile time
• A recursive inductive type refers to itself in its own constructors, enabling trees and other nested structures

i

-- Structure: a product type with named fields
structure Point where
  x : Float
  y : Float
  deriving Repr, BEq

-- Construct, access, and update
def origin : Point := { x := 0.0, y := 0.0 }

#eval origin.x                          -- 0.0
#eval { origin with x := 3.0 }         -- { x := 3.0, y := 0.0 }

-- Inductive: a sum type whose value is exactly one constructor
inductive Direction where
  | North | South | East | West
  deriving Repr, BEq

-- match must cover every constructor; Lean rejects incomplete matches
def opposite : Direction → Direction
  | Direction.North => Direction.South
  | Direction.South => Direction.North
  | Direction.East  => Direction.West
  | Direction.West  => Direction.East

#guard opposite Direction.North == Direction.South
#guard opposite (opposite Direction.East) == Direction.East

-- Constructors can carry data; each carries a different payload
inductive Shape where
  | Circle : Float → Shape
  | Rect   : Float → Float → Shape
  deriving Repr

def area : Shape → Float
  | Shape.Circle r   => 3.14159 * r * r
  | Shape.Rect w h   => w * h

#guard area (Shape.Rect 3.0 4.0) == 12.0
#guard area (Shape.Circle 1.0) == 3.14159

-- Recursive inductive: a binary tree refers to itself
inductive Tree where
  | Leaf : Tree
  | Node : Tree → Int → Tree → Tree
  deriving Repr

def treeSum : Tree → Int
  | Tree.Leaf         => 0
  | Tree.Node l v r   => treeSum l + v + treeSum r

--     2
--    / \
--   1   3
def sample : Tree :=
  Tree.Node
    (Tree.Node Tree.Leaf 1 Tree.Leaf)
    2
    (Tree.Node Tree.Leaf 3 Tree.Leaf)

#guard treeSum sample == 6

Exercises

Traffic Light

• Define inductive Light with constructors Red, Yellow, and Green
• Write next : Light → Light that cycles Red → Green → Yellow → Red
• Verify the full three-step cycle with #guard

Shape Area Extended

• Add a Triangle constructor to the Shape type carrying a base and height
• Extend the area function to handle it and verify with #guard that a triangle with base 6.0 and height 4.0 has area 12.0

Point Distance

• Define structure Point where x y : Float
• Write distance : Point → Point → Float using the Pythagorean theorem (Float.sqrt)
• Verify that the distance between (0, 0) and (3, 4) is 5.0

Tree Depth

• Using the Tree type from the lesson, write depth : Tree → Nat that returns the length of the longest path from root to leaf
• Verify that Tree.Leaf has depth 0 and sample from the lesson has depth 2