Type Classes

Define a type class to specify an interface that multiple types can satisfy
Write instance declarations to implement a type class for a specific type
Use [ClassName α] constraints to write functions that work for any type with an instance
Combine multiple constraints and extend classes with extends
Understand deriving as automatic instance generation

So far, deriving Repr and deriving BEq have appeared without full explanation
This lesson explains the mechanism behind them: type classes
Like Python's abstract base classes, but checked at compile time with no runtime overhead

Defining a Type Class

-- Define a type class with one required method
class Describable (α : Type) where
  describe : α → String

class Describable (α : Type) where introduces a new type class
- α is the type parameter — a placeholder for "whichever type implements this"
- describe : α → String is the required method: given a value, produce a string
Like Python's class Describable(ABC): @abstractmethod def describe(self) -> str: ...
- Unlike Python, the compiler enforces that every use has a valid implementation
No code is generated yet — class only defines the interface

Writing an Instance

-- An instance teaches Lean how to describe a specific type
instance : Describable Bool where
  describe b := if b then "yes" else "no"

instance : Describable Int where
  describe n := s!"the number {n}"

instance : Describable Bool where tells Lean how to satisfy Describable for Bool
- The body provides all required methods
instance : Describable Int where is a completely separate declaration for Int
Like registering a Python @singledispatch handler, but checked at compile time
Two types, two instances: Lean picks the right one based on the type of the argument

#eval Describable.describe true
#eval Describable.describe (42 : Int)

"yes"
"the number 42"

Describable.describe true resolves to the Bool instance at compile time
Describable.describe (42 : Int) resolves to the Int instance
No runtime dispatch: the choice is made during type-checking

Polymorphic Functions

-- [Describable α] is a constraint: α must have a Describable instance
def showAll [Describable α] (xs : List α) : String :=
  String.intercalate ", " (xs.map Describable.describe)

[Describable α] is a type class constraint
- Read as: "for any type α that has a Describable instance"
- Square brackets [...] distinguish class constraints from ordinary arguments (...)
showAll works for List Bool, List Int, or any list whose element type has an instance
Like a Python Generic function with a Protocol bound, but resolved at compile time

#eval showAll [true, false, true]
#eval showAll [(1 : Int), 2, 3]
#eval showAll ["hello", "world"]

"yes, no, yes"
"the number 1, the number 2, the number 3"
"'hello', 'world'"

The same function body handles Bool, Int, and String lists
- Lean selects the correct describe implementation for each call

Multiple Type Classes

-- Two independent type classes
class Describable (α : Type) where
  describe : α → String

class Weighable (α : Type) where
  weight : α → Nat

inductive Fruit where | Apple | Banana | Cherry
  deriving Repr

instance : Describable Fruit where
  describe
    | Fruit.Apple  => "apple"
    | Fruit.Banana => "banana"
    | Fruit.Cherry => "cherry"

instance : Weighable Fruit where
  weight
    | Fruit.Apple  => 180
    | Fruit.Banana => 120
    | Fruit.Cherry => 5

A single type can implement any number of classes
Fruit implements both Describable and Weighable independently
Like a Python class implementing multiple abstract base classes

-- A function can require multiple type class constraints
def report [Describable α] [Weighable α] (x : α) : String :=
  s!"{Describable.describe x} weighs {Weighable.weight x}g"

[Describable α] [Weighable α] requires both constraints
- The type must have instances for both classes to use report
The compiler verifies this at the call site — no runtime AttributeError

#eval report Fruit.Apple
#eval report Fruit.Banana
#eval report Fruit.Cherry

"apple weighs 180g"
"banana weighs 120g"
"cherry weighs 5g"

Extending Type Classes

-- extends inherits all methods of the parent class
class Describable (α : Type) where
  describe : α → String

class Verbose (α : Type) extends Describable α where
  verboseDescribe : α → String

extends Describable α means Verbose inherits describe from Describable
- An instance of Verbose automatically satisfies Describable
Like Python's class inheritance, but for interfaces rather than implementations

-- An instance of Verbose must provide both methods
instance : Verbose Int where
  describe n      := s!"{n}"
  verboseDescribe n :=
    if n < 0 then s!"negative: {n}"
    else if n == 0 then "zero"
    else s!"positive: {n}"

The instance must provide all methods: both describe (inherited requirement) and verboseDescribe

-- Any function expecting Describable also accepts Verbose
def label [Describable α] (x : α) : String :=
  s!"[{Describable.describe x}]"

#eval label (42 : Int)
#eval label (-7 : Int)
#eval Verbose.verboseDescribe (0 : Int)
#eval Verbose.verboseDescribe (5 : Int)

"[42]"
"[-7]"
"zero"
"positive: 5"

label only requires Describable, so Int (which has a Verbose instance) satisfies it
- A Verbose instance is also a Describable instance

`deriving` Revisited

-- Repr and BEq are type classes just like any user-defined class
-- deriving Repr generates an instance of the Repr class automatically
inductive Color where
  | Red | Green | Blue
  deriving Repr, BEq

Repr and BEq are ordinary type classes defined in the standard library
deriving Repr asks the compiler to generate a Repr Color instance automatically
- Lean can do this for any inductive type it fully understands
deriving BEq generates a BEq Color instance — structural equality
Not all classes can be derived: Describable cannot, because Lean does not know what string you want

-- Some classes cannot be derived — you write the instance by hand
class Describable (α : Type) where
  describe : α → String

instance : Describable Color where
  describe
    | Color.Red   => "red"
    | Color.Green => "green"
    | Color.Blue  => "blue"

-- Repr (from deriving) drives #eval output
#eval Color.Red
-- BEq (from deriving) enables ==
#guard Color.Red == Color.Red
#guard Color.Red != Color.Blue
-- Describable (written by hand) gives a custom string
#eval Describable.describe Color.Green

Color.Red
"green"

#eval Color.Red uses the auto-generated Repr instance
Color.Red == Color.Red uses the auto-generated BEq instance
Describable.describe Color.Green uses the hand-written instance
Whenever you see deriving X, there is a type class X behind it
- You can always write the instance yourself instead — deriving is just a shortcut

Exercises

Fix: Missing String Instance

-- Call showAll on a list of strings, but String has no Describable instance.
-- Add the missing instance so the guards pass.
class Describable (α : Type) where
  describe : α → String

instance : Describable Bool where
  describe b := if b then "yes" else "no"

instance : Describable Int where
  describe n := s!"the number {n}"

-- BUG: no instance for String, so showAll ["a", "b"] fails
def showAll [Describable α] (xs : List α) : String :=
  String.intercalate ", " (xs.map Describable.describe)

#guard showAll [true, false] == "yes, no"
#guard showAll [(1 : Int), 2] == "the number 1, the number 2"
#guard showAll ["a", "b"] == "a, b"

hint

showAll ["a", "b"] fails because there is no Describable String instance
Add an instance that returns the string itself: describe s := s
Like Python's __str__ for built-in types

Fix: Wrong Method Return Type

-- The Describable instance for Nat has the wrong method signature.
-- describe should return String, but this one returns Nat. Fix it.
class Describable (α : Type) where
  describe : α → String

-- BUG: describe returns Nat instead of String
instance : Describable Nat where
  describe n := n

#guard Describable.describe (0 : Nat) == "0"
#guard Describable.describe (42 : Nat) == "42"

hint

The class declares describe : α → String but the instance returns Nat
The return type must match the class declaration
Use s!"{n}" to convert the Nat to a String

Fix: Missing Type Class Constraint

-- report requires both Describable and Weighable constraints, but the
-- function signature only lists Describable. Add the missing constraint.
class Describable (α : Type) where
  describe : α → String

class Weighable (α : Type) where
  weight : α → Nat

inductive Fruit where | Apple | Banana
  deriving Repr

instance : Describable Fruit where
  describe | .Apple => "apple" | .Banana => "banana"

instance : Weighable Fruit where
  weight | .Apple => 180 | .Banana => 120

-- BUG: [Weighable α] constraint is missing
def report [Describable α] (x : α) : String :=
  s!"{Describable.describe x} weighs {Weighable.weight x}g"

#guard report Fruit.Apple == "apple weighs 180g"
#guard report Fruit.Banana == "banana weighs 120g"

hint

report uses Weighable.weight but the signature only lists [Describable α]
The compiler can't find the Weighable instance because you didn't ask for it
Add [Weighable α] as a second constraint in the square brackets

Fix: Missing Inherited Method

-- Verbose extends Describable, so an instance must provide both methods.
-- This instance only provides verboseDescribe. Add the missing method.
class Describable (α : Type) where
  describe : α → String

class Verbose (α : Type) extends Describable α where
  verboseDescribe : α → String

-- BUG: missing the inherited `describe` method
instance : Verbose Int where
  verboseDescribe n :=
    if n < 0 then s!"negative: {n}"
    else if n == 0 then "zero"
    else s!"positive: {n}"

#guard Describable.describe (42 : Int) == "42"
#guard Verbose.verboseDescribe (42 : Int) == "positive: 42"
#guard Verbose.verboseDescribe (-3 : Int) == "negative: -3"

hint

Verbose extends Describable, so the instance must provide describe AND verboseDescribe
The compiler error says which method is missing
Add describe n := s!"{n}" to the instance body

Fix: `deriving` Needs Parent Instances

-- trying to derive Repr on a type that uses a field without a Repr instance.
-- Repr can't be derived automatically here. Fix the error.
inductive Toy where
  | car
  | doll
  deriving Repr

-- BUG: MyBox can't derive Repr because Toy doesn't derive Repr
-- The error chain is: MyBox → needs Repr → Toy doesn't have it → fail
structure MyBox where
  toy : Toy
  label : String
  deriving Repr

#guard ({ toy := Toy.car, label := "red" : MyBox }).label == "red"

hint

MyBox tries to derive Repr, but its field toy : Toy needs Repr too
deriving chains: if a type contains another type, both must derive the class
Add deriving Repr to the Toy definition as well

Write: A `Summarizable` Class

-- Write a Summarizable type class with a `summary` method that returns
-- a one-line summary of a value. Then write an instance for String that
-- returns the first 10 characters followed by "..." if the string is longer.

class Summarizable (α : Type) where
  summary : α → String

-- TODO: write an instance for String

#guard Summarizable.summary "hello" == "hello"
#guard Summarizable.summary "hello world this is long" == "hello worl..."
#guard Summarizable.summary "" == ""

hint

Define instance : Summarizable String where …
If the string is 10 chars or shorter, return it as-is
Otherwise return s.extract 0 10 ++ "..." — use String.extract to slice

Write: A `Doubleable` Class

-- Write a Doubleable type class with a `twice` method that returns
-- the doubled value. Then write an instance for Nat.

class Doubleable (α : Type) where
  twice : α → α

-- TODO: write an instance for Nat

#guard Doubleable.twice (0 : Nat) == 0
#guard Doubleable.twice (21 : Nat) == 42
#guard Doubleable.twice (100 : Nat) == 200

hint

Define instance : Doubleable Nat where …
The twice method should multiply by 2: twice n := n * 2
Simple arithmetic: this is the "hello world" of type class instances

Write: A Function with Two Constraints

-- Write a function `describeWeight` that has BOTH Describable and Weighable
-- constraints and returns a string like "an apple weighs 180g".

class Describable (α : Type) where
  describe : α → String

class Weighable (α : Type) where
  weight : α → Nat

inductive Fruit where | Apple | Banana
  deriving Repr

instance : Describable Fruit where
  describe | .Apple => "an apple" | .Banana => "a banana"

instance : Weighable Fruit where
  weight | .Apple => 180 | .Banana => 120

-- TODO: write describeWeight with both constraints
def describeWeight (x : Fruit) : String :=
  ""

#guard describeWeight Fruit.Apple == "an apple weighs 180g"
#guard describeWeight Fruit.Banana == "a banana weighs 120g"

hint

Change the signature to def describeWeight [Describable α] [Weighable α] (x : α) : String
Use Describable.describe x for the name and Weighable.weight x for the weight
Format with s!"{...} weighs {...}g"

Write: Extend a Class

-- Extend the Measurable class with a Comparable class that adds
-- a `biggerThan` method. Write an instance for Nat.

class Measurable (α : Type) where
  size : α → Nat

class Comparable (α : Type) extends Measurable α where
  biggerThan : α → α → Bool

-- TODO: write an instance of Comparable for Nat

#guard Measurable.size (42 : Nat) == 42
#guard Comparable.biggerThan (10 : Nat) (5 : Nat) == true
#guard Comparable.biggerThan (3 : Nat) (7 : Nat) == false

hint

Write instance : Comparable Nat where …
size n := n — the size of a Nat is itself
biggerThan a b := a > b — use the built-in > operator
Both methods must be provided; Comparable inherits size from Measurable

Write: A Manual Display Instance

-- Instead of deriving Repr, write a manual Display instance for the
-- TrafficLight type. The `display` method should return the colour name.

class Display (α : Type) where
  display : α → String

inductive TrafficLight where
  | Red | Yellow | Green

-- TODO: write a manual instance of Display for TrafficLight
-- (do NOT use deriving)

#guard Display.display TrafficLight.Red == "red"
#guard Display.display TrafficLight.Yellow == "yellow"
#guard Display.display TrafficLight.Green == "green"

hint

Write instance : Display TrafficLight where …
Use pattern matching on the three constructors
| .Red => "red", | .Yellow => "yellow", | .Green => "green"
This is what deriving Repr does automatically — you're doing it by hand

Type Classes

Defining a Type Class

Writing an Instance

Polymorphic Functions

Multiple Type Classes

Extending Type Classes

deriving Revisited

Exercises

Fix: Missing String Instance

Fix: Wrong Method Return Type

Fix: Missing Type Class Constraint

Fix: Missing Inherited Method

Fix: deriving Needs Parent Instances

Write: A Summarizable Class

Write: A Doubleable Class

Write: A Function with Two Constraints

Write: Extend a Class

Write: A Manual Display Instance

`deriving` Revisited

Fix: `deriving` Needs Parent Instances

Write: A `Summarizable` Class

Write: A `Doubleable` Class