Type classes In Lean

Explaining Leans type system using my knowledge of Rust. Say you a circle or a square. They are not the same thing but they are both geometric shapes. They have common properties like they both have area. In rust we want to define a trait Shape, and in Lean we have a class Shape. Then we have both circle and square implement Shape, and in Lean we say circle and square are instances of class Shape.

Here the concrete object is Point and the general trait it satisfies is that is a thing that is an instance of the MyAdd class i.e. it is a thing that can be added to itself.

Plain English	Lean	Rust
Define an interface	class	trait
Implement it for Point	instance : MyAdd Point	impl MyAdd for Point
“α/T must support addition”	[MyAdd α] binder	<T: MyAdd> bound
Find the right implementation	Instance database	Trait impl resolution

The rest of these notes fill in the details and differences.

The Problem#

Let’s define a Point and Point3D and try to double it:

structure Point where
  x : Float
  y : Float

structure Point3D where
  x : Float
  y : Float
  z : Float

def double (x : Point) : Point := x + x   -- error: no + on Point

This fails. What does + mean for a Point? Lean has no idea. We need to tell Lean what it means for a term of type Point to be added itself.

So we define an explicit function that adds two points.

def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

def double (x : Point) : Point := addPoints x x  -- works

But what happens if we wanted to define doubling for Point3D. We can’t use double as its hard coded to use addPoints which is hard coded to use arguments with terms of type Point. In Rust we use traits for this. We will soon see that Lean offers similar functionality - via classes.

trait MyAdd {
    fn add(self, other: Self) -> Self;
}

impl MyAdd for Point {
    fn add(self, other: Point) -> Point {
        Point { x: self.x + other.x, y: self.y + other.y }
    }
}

impl MyAdd for Point3D {
    fn add(self, other: Point3D) -> Point3D {
        Point3D { x: self.x + other.x, y: self.y + other.y, z: self.z + other.z }
    }
}

fn double<T: MyAdd + Copy>(x: T) -> T { x.add(x) }

double(point);     // compiler finds impl MyAdd for Point
double(point3d);   // compiler finds impl MyAdd for Point3D

Classes — Traits In Lean#

A Lean class looks identical to a structure:

class MyAdd (α : Type) where
  add : α → α → α

We already saw the Rust impl blocks above. In Lean the equivalent is instance. In Rust we say this type implements this trait. In Lean we say this type is an instance of this class.

def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

def addPoints3D (p1 : Point3D) (p2 : Point3D) : Point3D :=
  { x := p1.x + p2.x, y := p1.y + p2.y, z := p1.z + p2.z }

instance : MyAdd Point where
  add := addPoints

instance : MyAdd Point3D where
  add := addPoints3D

instance : MyAdd ℕ where
  add := Nat.add

MyAdd has one field (add), so each instance provides one function — just like the Rust trait MyAdd had one method. If a class has multiple fields, you provide all of them:

class MyArith (α : Type) where
  add : α → α → α
  mul : α → α → α

instance : MyArith ℕ where
  add := Nat.add
  mul := Nat.mul

Lean stores these in an instance database — a lookup table that maps (class, type) pairs to their implementations. When Lean needs MyAdd Point, it searches this database and finds the instance we defined. Same idea as how the Rust compiler resolves which impl to use for a given type.

Instance Implicit Arguments [ ] — Trait Bounds#

Now that instances are registered in the database, we write

def double [MyAdd α] (x : α) : α := MyAdd.add x x

Without [MyAdd α], α could be any type — and MyAdd.add wouldn’t be defined for an arbitrary α. The [MyAdd α] restricts α to only terms of types that have a MyAdd instance registered. When double is called with x : Point or x : Point3D, the elaborator checks the instance database for a matching MyAdd entry for that type.

double { x := 1.0, y := 2.0 }                  -- Lean finds MyAdd Point automatically
double { x := 1.0, y := 2.0, z := 3.0 }        -- Lean finds MyAdd Point3D automatically
double (5 : ℕ)                                  -- Lean finds MyAdd ℕ automatically

Same idea works for MyArith with multiple fields:

def mulPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x * p2.x, y := p1.y * p2.y }

instance : MyArith Point where
  add := addPoints
  mul := mulPoints

-- unnamed: access fields via the class name
def squareAndAdd [MyArith α] (x : α) : α := MyArith.add (MyArith.mul x x) x

-- named: h is a variable bound to the concrete impl of MyArith for α. Access its fields via h.
def squareAndAdd [h : MyArith α] (x : α) : α := h.add (h.mul x x) x

squareAndAdd { x := 2.0, y := 3.0 }   -- Lean finds MyArith Point
squareAndAdd (5 : ℕ)                   -- Lean finds MyArith ℕ

When you write double { x := 1.0, y := 2.0 }, Lean:

1. Sees the argument is a Point
2. Sees it needs [MyAdd Point]
3. Searches the instance database
4. Finds instance : MyAdd Point
5. Inserts it silently

Accessing Fields#

In Rust you call trait methods on the value: x.add(y). In Lean you call them via the class name: MyAdd.add x y. In practice, Mathlib registers operator notation so you just write x + y directly, same as Rust’s operator overloading via impl Add.

extends — Trait Inheritance#

In Rust, trait inheritance looks like: This is saying any type that implements AddMonoid must also implement the traits Add and Zero.

trait AddMonoid: Add + Zero {
    fn add_assoc(a: Self, b: Self, c: Self) -> bool;
}

In Lean, extends does the same. Note that α plays the role of Self in Rust — it’s the type the class is being implemented for:

α is a term of type Type that is an instance of class AddMonoid. α is ALSO an instance of class Add and Zero.

class AddMonoid (α : Type) extends Add α, Zero α where
  add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)  -- term of Prop (a proof)
  zero_add  : ∀ (a : α), 0 + a = a                    -- term of Prop (a proof)
  add_zero  : ∀ (a : α), a + 0 = a                    -- term of Prop (a proof)
-- α here is like Self. When you write instance : AddMonoid ℕ, α = ℕ.
-- extends Add α gives us: add : α → α → α             -- term of Type (a function)
-- extends Zero α gives us: zero : α                    -- term of Type (a value)
--
-- To verify, type these into Lean:
-- #check @AddMonoid.add_assoc   -- ∀ ... → Prop
-- #check @Add.add               -- α → α → α

AddMonoid α gives you Add α and Zero α automatically, plus the axioms.

The critical difference from Rust: the fields can be proofs. add_assoc is not a function returning bool — it is a term of a Prop type (recall: Prop is Sort 0, the universe of propositions). Providing this field means constructing a term that proves associativity holds. This is something Rust traits fundamentally cannot express.

A Ring extends further with multiplication, negation, and all ring axioms. By the time you write [Ring α], Lean has +, *, -, 0, 1, and proofs of all the ring laws — bundled into one instance.

Associated Types — Extra Parameters Instead#

Rust uses associated types when a trait’s output type depends on the input:

struct Point { x: f64, y: f64 }

trait Add<Rhs = Self> {
    type Output;
    fn add(self, rhs: Rhs) -> Self::Output;
}

// Point + Point → Point
impl Add for Point {
    type Output = Point;
    fn add(self, rhs: Point) -> Point {
        Point { x: self.x + rhs.x, y: self.y + rhs.y }
    }
}

// Point + f64 → Point (shift both fields by a scalar)
impl Add<f64> for Point {
    type Output = Point;
    fn add(self, rhs: f64) -> Point {
        Point { x: self.x + rhs, y: self.y + rhs }
    }
}

Lean doesn’t have associated types. Instead, it uses extra type parameters:

class HAdd (α : Type) (β : Type) (γ : Type) where
  hAdd : α → β → γ

-- adding two Points gives a Point
instance : HAdd Point Point Point where
  hAdd := addPoints

-- adding a Point and a Float scales both fields
instance : HAdd Point Float Point where
  hAdd := fun p s => { x := p.x + s, y := p.y + s }

Same result, different encoding. Rust bakes the output type into the trait with type Output. Lean just adds more type parameters.

What [Ring α] Means In A Theorem#

theorem foo [Ring α] (x y : α) : (x + y) * (x - y) = x ^ 2 - y ^ 2 := by
  ring

This is like a Rust generic function with a Ring bound — it works for any type α that implements Ring. Lean finds the Ring ℝ instance when you use it with ℝ, silently.

If you tried ℕ, Lean fails — there is no Ring ℕ instance because ℕ has no additive inverses (it does have CommSemiring, just not a full ring). Same as how Rust would reject double::<u32>() if u32 didn’t implement your trait.

Instance Chaining#

We defined MyArith with both add and mul. We also defined MyAdd with just add. Any type that has MyArith clearly also has MyAdd — it already has an add function. We can tell Lean this:

instance [MyArith α] : MyAdd α where
  add := MyArith.add
-- "if α implements MyArith, it automatically implements MyAdd"
-- You must register this rule explicitly. Without it, having MyArith Point
-- tells Lean nothing about MyAdd Point — the chaining doesn't happen by magic.

This is like a Rust blanket impl:

impl<T: MyArith> MyAdd for T {
    fn add(self, other: T) -> T { MyArith::add(self, other) }
}

Now say we have MyArith Point registered but no direct MyAdd Point:

instance : MyArith Point where
  add := addPoints
  mul := mulPoints

-- We do NOT register MyAdd for Point:
-- instance : MyAdd Point where
--   add := addPoints

-- But double still works! It needs [MyAdd Point], which it gets
-- from the chaining rule we registered above.
double { x := 1.0, y := 2.0 }   -- ✓

Lean chains the instances:

1. Needs [MyAdd Point] — not found directly
2. Finds the rule: [MyArith α] → MyAdd α
3. Searches for [MyArith Point] — found
4. Chains them: MyArith Point → MyAdd Point

We never wrote instance : MyAdd Point — Lean derived it from MyArith Point. In Mathlib this chaining goes dozens of layers deep (e.g. Field → Ring → AddGroup → Add).

Reading The Infoview: What Is inst✝?#

Paste this into Lean and place your cursor on sorry:

-- Example 1: using our MyAdd class
def double [MyAdd α] (x : α) : α := by
  sorry
-- Infoview shows:
-- α : Type
-- inst✝ : MyAdd α
-- x : α
-- ⊢ α

-- Example 2: using MyArith with two fields
def squareAndAdd [MyArith α] (x : α) : α := by
  sorry
-- Infoview shows:
-- α : Type
-- inst✝ : MyArith α
-- x : α
-- ⊢ α

-- Example 3: naming the instance
def double [h : MyAdd α] (x : α) : α := by
  sorry
-- Infoview shows:
-- α : Type
-- h : MyAdd α      ← named, no ✝
-- x : α
-- ⊢ α

inst✝ is the auto-generated name for the resolved impl. The ✝ dagger means Lean named it because you didn’t — you wrote [MyAdd α] (anonymous). If you write [h : MyAdd α], it shows as h instead.

The impl is a real value in your context. inst✝ : MyAdd α means you have access to inst✝.add (or equivalently MyAdd.add). In Rust terms, it’s as if the compiler showed you the resolved impl block as a local variable.

Full Code#

Two files you can paste into a Lean project and run.

File 1: Typeclasses.lean — structures, classes, instances, chaining#

-- ============================================================
-- Structures (data types)
-- ============================================================

structure Point where
  x : Float
  y : Float
  deriving Repr

structure Point3D where
  x : Float
  y : Float
  z : Float
  deriving Repr

-- ============================================================
-- Addition functions (one per type — the logic differs)
-- ============================================================

def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

def addPoints3D (p1 : Point3D) (p2 : Point3D) : Point3D :=
  { x := p1.x + p2.x, y := p1.y + p2.y, z := p1.z + p2.z }

def mulPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x * p2.x, y := p1.y * p2.y }

-- ============================================================
-- Class definitions (like Rust traits)
-- ============================================================

class MyAdd (α : Type) where
  add : α → α → α

class MyArith (α : Type) where
  add : α → α → α
  mul : α → α → α

-- ============================================================
-- Instances (like Rust impl blocks)
-- ============================================================

instance : MyAdd Point where
  add := addPoints

instance : MyAdd Point3D where
  add := addPoints3D

instance : MyAdd Nat where
  add := Nat.add

instance : MyArith Nat where
  add := Nat.add
  mul := Nat.mul

instance : MyArith Point where
  add := addPoints
  mul := mulPoints

-- ============================================================
-- Instance chaining: MyArith → MyAdd
-- Must be registered explicitly. Without this line,
-- having MyArith α tells Lean nothing about MyAdd α.
-- ============================================================

instance [MyArith α] : MyAdd α where
  add := MyArith.add

-- ============================================================
-- Functions using [ ] (instance implicit / trait bounds)
-- ============================================================

def double [MyAdd α] (x : α) : α := MyAdd.add x x

def squareAndAdd [MyArith α] (x : α) : α := MyArith.add (MyArith.mul x x) x

-- ============================================================
-- Usage — Lean looks up the instance automatically
-- ============================================================

#eval double { x := 1.0, y := 2.0 : Point }
-- { x := 2.000000, y := 4.000000 }

#eval double { x := 1.0, y := 2.0, z := 3.0 : Point3D }
-- { x := 2.000000, y := 4.000000, z := 6.000000 }

#eval double (5 : Nat)
-- 10

#eval squareAndAdd (3 : Nat)
-- 12

#eval squareAndAdd { x := 2.0, y := 3.0 : Point }
-- { x := 6.000000, y := 12.000000 }

-- ============================================================
-- Instance search failure examples
-- ============================================================

-- This would fail: no MyAdd instance for String
-- #eval double "hello"
-- Error: failed to synthesize MyAdd String

-- This would fail: no MyArith instance for Point3D
-- #eval squareAndAdd { x := 1.0, y := 2.0, z := 3.0 : Point3D }
-- Error: failed to synthesize MyArith Point3D
-- Fix: register instance : MyArith Point3D

File 2: TypeclassesChaining.lean — chaining in action#

-- This file demonstrates that chaining lets you skip
-- writing MyAdd instances when MyArith is already registered.

structure Vec2 where
  x : Float
  y : Float
  deriving Repr

def addVec2 (a b : Vec2) : Vec2 := { x := a.x + b.x, y := a.y + b.y }
def mulVec2 (a b : Vec2) : Vec2 := { x := a.x * b.x, y := a.y * b.y }

class MyAdd (α : Type) where
  add : α → α → α

class MyArith (α : Type) where
  add : α → α → α
  mul : α → α → α

-- Register the chaining rule: MyArith implies MyAdd
instance [MyArith α] : MyAdd α where
  add := MyArith.add

-- Only register MyArith for Vec2 — NOT MyAdd
instance : MyArith Vec2 where
  add := addVec2
  mul := mulVec2

-- We never wrote: instance : MyAdd Vec2

def double [MyAdd α] (x : α) : α := MyAdd.add x x

-- This works! Lean chains MyArith Vec2 → MyAdd Vec2
#eval double { x := 3.0, y := 4.0 : Vec2 }
-- { x := 6.000000, y := 8.000000 }

-- Now comment out the chaining rule above and this line fails:
-- Error: failed to synthesize MyAdd Vec2
-- Because without the rule, Lean has no way to get MyAdd from MyArith.