# Type Classes

Type classes were introduced as a principled way of enabling ad-hoc polymorphism in functional programming languages. We first observe that it would be easy to implement an ad-hoc polymorphic function (such as addition) if the function simply took the type-specific implementation of addition as an argument and then called that implementation on the remaining arguments. For example, suppose we declare a structure in Lean to hold implementations of addition.

```
namespace Ex
structure Add (a : Type) where
add : a → a → a
#check @Add.add
-- Add.add : {a : Type} → Add a → a → a → a
end Ex
```

In the above Lean code, the field `add`

has type
`Add.add : {a : Type} → Add a → a → a → a`

where the curly braces around the type `a`

mean that it is an implicit argument.
We could implement `double`

by:

```
namespace Ex
structure Add (a : Type) where
add : a → a → a
def double (s : Add a) (x : a) : a :=
s.add x x
#eval double { add := Nat.add } 10
-- 20
#eval double { add := Nat.mul } 10
-- 100
#eval double { add := Int.add } 10
-- 20
end Ex
```

Note that you can double a natural number `n`

by `double { add := Nat.add } n`

.
Of course, it would be highly cumbersome for users to manually pass the
implementations around in this way.
Indeed, it would defeat most of the potential benefits of ad-hoc
polymorphism.

The main idea behind type classes is to make arguments such as `Add a`

implicit,
and to use a database of user-defined instances to synthesize the desired instances
automatically through a process known as typeclass resolution. In Lean, by changing
`structure`

to `class`

in the example above, the type of `Add.add`

becomes:

```
namespace Ex
class Add (a : Type) where
add : a → a → a
#check @Add.add
-- Add.add : {a : Type} → [self : Add a] → a → a → a
end Ex
```

where the square brackets indicate that the argument of type `Add a`

is *instance implicit*,
i.e. that it should be synthesized using typeclass resolution. This version of
`add`

is the Lean analogue of the Haskell term `add :: Add a => a -> a -> a`

.
Similarly, we can register instances by:

```
namespace Ex
class Add (a : Type) where
add : a → a → a
instance : Add Nat where
add := Nat.add
instance : Add Int where
add := Int.add
instance : Add Float where
add := Float.add
end Ex
```

Then for `n : Nat`

and `m : Nat`

, the term `Add.add n m`

triggers typeclass resolution with
the goal of `Add Nat`

, and typeclass resolution will synthesize the instance for `Nat`

above.
We can now reimplement `double`

using an instance implicit by:

```
namespace Ex
class Add (a : Type) where
add : a → a → a
instance : Add Nat where
add := Nat.add
instance : Add Int where
add := Int.add
instance : Add Float where
add := Float.add
def double [Add a] (x : a) : a :=
Add.add x x
#check @double
-- @double : {a : Type} → [inst : Add a] → a → a
#eval double 10
-- 20
#eval double (10 : Int)
-- 100
#eval double (7 : Float)
-- 14.000000
#eval double (239.0 + 2)
-- 482.000000
end Ex
```

In general, instances may depend on other instances in complicated ways. For example,
you can declare an (anonymous) instance stating that if `a`

has addition, then `Array a`

has addition:

```
instance [Add a] : Add (Array a) where
add x y := Array.zipWith x y (· + ·)
#eval Add.add #[1, 2] #[3, 4]
-- #[4, 6]
#eval #[1, 2] + #[3, 4]
-- #[4, 6]
```

Note that `(· + ·)`

is notation for `fun x y => x + y`

in Lean.

The example above demonstrates how type classes are used to overload notation.
Now, we explore another application. We often need an arbitrary element of a given type.
Recall that types may not have any elements in Lean.
It often happens that we would like a definition to return an arbitrary element in a "corner case."
For example, we may like the expression `head xs`

to be of type `a`

when `xs`

is of type `List a`

.
Similarly, many theorems hold under the additional assumption that a type is not empty.
For example, if `a`

is a type, `exists x : a, x = x`

is true only if `a`

is not empty.
The standard library defines a type class `Inhabited`

to enable type class inference to infer a
"default" element of an inhabited type.
Let us start with the first step of the program above, declaring an appropriate class:

```
namespace Ex
class Inhabited (a : Type u) where
default : a
#check @Inhabited.default
-- Inhabited.default : {a : Type u} → [self : Inhabited a] → a
end Ex
```

Note `Inhabited.default`

doesn't have any explicit arguments.

An element of the class `Inhabited a`

is simply an expression of the form `Inhabited.mk x`

, for some element `x : a`

.
The projection `Inhabited.default`

will allow us to "extract" such an element of `a`

from an element of `Inhabited a`

.
Now we populate the class with some instances:

```
namespace Ex
class Inhabited (a : Type _) where
default : a
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
instance : Inhabited Unit where
default := ()
instance : Inhabited Prop where
default := True
#eval (Inhabited.default : Nat)
-- 0
#eval (Inhabited.default : Bool)
-- true
end Ex
```

You can use the command `export`

to create the alias `default`

for `Inhabited.default`

```
namespace Ex
class Inhabited (a : Type _) where
default : a
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
instance : Inhabited Unit where
default := ()
instance : Inhabited Prop where
default := True
export Inhabited (default)
#eval (default : Nat)
-- 0
#eval (default : Bool)
-- true
end Ex
```

## Chaining Instances

If that were the extent of type class inference, it would not be all that impressive;
it would be simply a mechanism of storing a list of instances for the elaborator to find in a lookup table.
What makes type class inference powerful is that one can *chain* instances. That is,
an instance declaration can in turn depend on an implicit instance of a type class.
This causes class inference to chain through instances recursively, backtracking when necessary, in a Prolog-like search.

For example, the following definition shows that if two types `a`

and `b`

are inhabited, then so is their product:

```
instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
default := (default, default)
```

With this added to the earlier instance declarations, type class instance can infer, for example, a default element of `Nat × Bool`

:

```
namespace Ex
class Inhabited (a : Type u) where
default : a
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
opaque default [Inhabited a] : a :=
Inhabited.default
instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
default := (default, default)
#eval (default : Nat × Bool)
-- (0, true)
end Ex
```

Similarly, we can inhabit type function with suitable constant functions:

```
instance [Inhabited b] : Inhabited (a → b) where
default := fun _ => default
```

As an exercise, try defining default instances for other types, such as `List`

and `Sum`

types.

The Lean standard library contains the definition `inferInstance`

. It has type `{α : Sort u} → [i : α] → α`

,
and is useful for triggering the type class resolution procedure when the expected type is an instance.

```
#check (inferInstance : Inhabited Nat) -- Inhabited Nat
def foo : Inhabited (Nat × Nat) :=
inferInstance
theorem ex : foo.default = (default, default) :=
rfl
```

You can use the command `#print`

to inspect how simple `inferInstance`

is.

```
#print inferInstance
```

## ToString

The polymorphic method `toString`

has type `{α : Type u} → [ToString α] → α → String`

. You implement the instance
for your own types and use chaining to convert complex values into strings. Lean comes with `ToString`

instances
for most builtin types.

```
structure Person where
name : String
age : Nat
instance : ToString Person where
toString p := p.name ++ "@" ++ toString p.age
#eval toString { name := "Leo", age := 542 : Person }
#eval toString ({ name := "Daniel", age := 18 : Person }, "hello")
```

## Numerals

Numerals are polymorphic in Lean. You can use a numeral (e.g., `2`

) to denote an element of any type that implements
the type class `OfNat`

.

```
structure Rational where
num : Int
den : Nat
inv : den ≠ 0
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := by decide }
instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"
#eval (2 : Rational) -- 2/1
#check (2 : Rational) -- Rational
#check (2 : Nat) -- Nat
```

Lean elaborates the terms `(2 : Nat)`

and `(2 : Rational)`

as
`OfNat.ofNat Nat 2 (instOfNatNat 2)`

and
`OfNat.ofNat Rational 2 (instOfNatRational 2)`

respectively.
We say the numerals `2`

occurring in the elaborated terms are *raw* natural numbers.
You can input the raw natural number `2`

using the macro `nat_lit 2`

.

```
#check nat_lit 2 -- Nat
```

Raw natural numbers are *not* polymorphic.

The `OfNat`

instance is parametric on the numeral. So, you can define instances for particular numerals.
The second argument is often a variable as in the example above, or a *raw* natural number.

```
class Monoid (α : Type u) where
unit : α
op : α → α → α
instance [s : Monoid α] : OfNat α (nat_lit 1) where
ofNat := s.unit
def getUnit [Monoid α] : α :=
1
```

## Output Parameters

By default, Lean only tries to synthesize an instance `Inhabited T`

when the term `T`

is known and does not
contain missing parts. The following command produces the error
"typeclass instance problem is stuck, it is often due to metavariables `?m.7`

" because the type has a missing part (i.e., the `_`

).

```
#check_failure (inferInstance : Inhabited (Nat × _))
```

You can view the parameter of the type class `Inhabited`

as an *input* value for the type class synthesizer.
When a type class has multiple parameters, you can mark some of them as output parameters.
Lean will start type class synthesizer even when these parameters have missing parts.
In the following example, we use output parameters to define a *heterogeneous* polymorphic
multiplication.

```
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
instance : HMul Nat Nat Nat where
hMul := Nat.mul
instance : HMul Nat (Array Nat) (Array Nat) where
hMul a bs := bs.map (fun b => hMul a b)
#eval hMul 4 3 -- 12
#eval hMul 4 #[2, 3, 4] -- #[8, 12, 16]
end Ex
```

The parameters `α`

and `β`

are considered input parameters and `γ`

an output one.
Given an application `hMul a b`

, after the types of `a`

and `b`

are known, the type class
synthesizer is invoked, and the resulting type is obtained from the output parameter `γ`

.
In the example above, we defined two instances. The first one is the homogeneous
multiplication for natural numbers. The second is the scalar multiplication for arrays.
Note that you chain instances and generalize the second instance.

```
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
instance : HMul Nat Nat Nat where
hMul := Nat.mul
instance : HMul Int Int Int where
hMul := Int.mul
instance [HMul α β γ] : HMul α (Array β) (Array γ) where
hMul a bs := bs.map (fun b => hMul a b)
#eval hMul 4 3 -- 12
#eval hMul 4 #[2, 3, 4] -- #[8, 12, 16]
#eval hMul (-2) #[3, -1, 4] -- #[-6, 2, -8]
#eval hMul 2 #[#[2, 3], #[0, 4]] -- #[#[4, 6], #[0, 8]]
end Ex
```

You can use our new scalar array multiplication instance on arrays of type `Array β`

with a scalar of type `α`

whenever you have an instance `HMul α β γ`

.
In the last `#eval`

, note that the instance was used twice on an array of arrays.

## Default Instances

In the class `HMul`

, the parameters `α`

and `β`

are treated as input values.
Thus, type class synthesis only starts after these two types are known. This may often
be too restrictive.

```
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
instance : HMul Int Int Int where
hMul := Int.mul
def xs : List Int := [1, 2, 3]
-- Error "typeclass instance problem is stuck, it is often due to metavariables HMul ?m.89 ?m.90 ?m.91"
#check_failure fun y => xs.map (fun x => hMul x y)
end Ex
```

The instance `HMul`

is not synthesized by Lean because the type of `y`

has not been provided.
However, it is natural to assume that the type of `y`

and `x`

should be the same in
this kind of situation. We can achieve exactly that using *default instances*.

```
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
@[default_instance]
instance : HMul Int Int Int where
hMul := Int.mul
def xs : List Int := [1, 2, 3]
#check fun y => xs.map (fun x => hMul x y) -- Int → List Int
end Ex
```

By tagging the instance above with the attribute `default_instance`

, we are instructing Lean
to use this instance on pending type class synthesis problems.
The actual Lean implementation defines homogeneous and heterogeneous classes for arithmetical operators.
Moreover, `a+b`

, `a*b`

, `a-b`

, `a/b`

, and `a%b`

are notations for the heterogeneous versions.
The instance `OfNat Nat n`

is the default instance (with priority 100) for the `OfNat`

class. This is why the numeral
`2`

has type `Nat`

when the expected type is not known. You can define default instances with higher
priority to override the builtin ones.

```
structure Rational where
num : Int
den : Nat
inv : den ≠ 0
@[default_instance 200]
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := by decide }
instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"
#check 2 -- Rational
```

Priorities are also useful to control the interaction between different default instances.
For example, suppose `xs`

has type `List α`

. When elaborating `xs.map (fun x => 2 * x)`

, we want the homogeneous instance for multiplication
to have higher priority than the default instance for `OfNat`

. This is particularly important when we have implemented only the instance
`HMul α α α`

, and did not implement `HMul Nat α α`

.
Now, we reveal how the notation `a*b`

is defined in Lean.

```
namespace Ex
class OfNat (α : Type u) (n : Nat) where
ofNat : α
@[default_instance]
instance (n : Nat) : OfNat Nat n where
ofNat := n
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
class Mul (α : Type u) where
mul : α → α → α
@[default_instance 10]
instance [Mul α] : HMul α α α where
hMul a b := Mul.mul a b
infixl:70 " * " => HMul.hMul
end Ex
```

The `Mul`

class is convenient for types that only implement the homogeneous multiplication.

## Local Instances

Type classes are implemented using attributes in Lean. Thus, you can
use the `local`

modifier to indicate that they only have effect until
the current `section`

or `namespace`

is closed, or until the end
of the current file.

```
structure Point where
x : Nat
y : Nat
section
local instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end -- instance `Add Point` is not active anymore
-- def triple (p : Point) :=
-- p + p + p -- Error: failed to synthesize instance
```

You can also temporarily disable an instance using the `attribute`

command
until the current `section`

or `namespace`

is closed, or until the end
of the current file.

```
structure Point where
x : Nat
y : Nat
instance addPoint : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
attribute [-instance] addPoint
-- def triple (p : Point) :=
-- p + p + p -- Error: failed to synthesize instance
```

We recommend you only use this command to diagnose problems.

## Scoped Instances

You can also declare scoped instances in namespaces. This kind of instance is only active when you are inside of the namespace or open the namespace.

```
structure Point where
x : Nat
y : Nat
namespace Point
scoped instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end Point
-- instance `Add Point` is not active anymore
-- #check fun (p : Point) => p + p + p -- Error
namespace Point
-- instance `Add Point` is active again
#check fun (p : Point) => p + p + p
end Point
open Point -- activates instance `Add Point`
#check fun (p : Point) => p + p + p
```

You can use the command `open scoped <namespace>`

to activate scoped attributes but will
not "open" the names from the namespace.

```
structure Point where
x : Nat
y : Nat
namespace Point
scoped instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end Point
open scoped Point -- activates instance `Add Point`
#check fun (p : Point) => p + p + p
-- #check fun (p : Point) => double p -- Error: unknown identifier 'double'
```

## Decidable Propositions

Let us consider another example of a type class defined in the
standard library, namely the type class of `Decidable`

propositions. Roughly speaking, an element of `Prop`

is said to be
decidable if we can decide whether it is true or false. The
distinction is only useful in constructive mathematics; classically,
every proposition is decidable. But if we use the classical principle,
say, to define a function by cases, that function will not be
computable. Algorithmically speaking, the `Decidable`

type class can
be used to infer a procedure that effectively determines whether or
not the proposition is true. As a result, the type class supports such
computational definitions when they are possible while at the same
time allowing a smooth transition to the use of classical definitions
and classical reasoning.

In the standard library, `Decidable`

is defined formally as follows:

```
namespace Hidden
class inductive Decidable (p : Prop) where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p
end Hidden
```

Logically speaking, having an element `t : Decidable p`

is stronger
than having an element `t : p ∨ ¬p`

; it enables us to define values
of an arbitrary type depending on the truth value of `p`

. For
example, for the expression `if p then a else b`

to make sense, we
need to know that `p`

is decidable. That expression is syntactic
sugar for `ite p a b`

, where `ite`

is defined as follows:

```
namespace Hidden
def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => t)
end Hidden
```

The standard library also contains a variant of `ite`

called
`dite`

, the dependent if-then-else expression. It is defined as
follows:

```
namespace Hidden
def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
Decidable.casesOn (motive := fun _ => α) h e t
end Hidden
```

That is, in `dite c t e`

, we can assume `hc : c`

in the "then"
branch, and `hnc : ¬ c`

in the "else" branch. To make `dite`

more
convenient to use, Lean allows us to write `if h : c then t else e`

instead of `dite c (λ h : c => t) (λ h : ¬ c => e)`

.

Without classical logic, we cannot prove that every proposition is
decidable. But we can prove that *certain* propositions are
decidable. For example, we can prove the decidability of basic
operations like equality and comparisons on the natural numbers and
the integers. Moreover, decidability is preserved under propositional
connectives:

```
#check @instDecidableAnd
-- {p q : Prop} → [Decidable p] → [Decidable q] → Decidable (And p q)
#check @instDecidableOr
#check @instDecidableNot
```

Thus we can carry out definitions by cases on decidable predicates on the natural numbers:

```
def step (a b x : Nat) : Nat :=
if x < a ∨ x > b then 0 else 1
set_option pp.explicit true
#print step
```

Turning on implicit arguments shows that the elaborator has inferred
the decidability of the proposition `x < a ∨ x > b`

, simply by
applying appropriate instances.

With the classical axioms, we can prove that every proposition is
decidable. You can import the classical axioms and make the generic
instance of decidability available by opening the `Classical`

namespace.

```
open Classical
```

Thereafter `Decidable p`

has an instance for every `p`

.
Thus all theorems in the library
that rely on decidability assumptions are freely available when you
want to reason classically. In Chapter Axioms and Computation,
we will see that using the law of the
excluded middle to define functions can prevent them from being used
computationally. Thus, the standard library assigns a low priority to
the `propDecidable`

instance.

```
namespace Hidden
open Classical
noncomputable scoped
instance (priority := low) propDecidable (a : Prop) : Decidable a :=
choice <| match em a with
| Or.inl h => ⟨isTrue h⟩
| Or.inr h => ⟨isFalse h⟩
end Hidden
```

This guarantees that Lean will favor other instances and fall back on
`propDecidable`

only after other attempts to infer decidability have
failed.

The `Decidable`

type class also provides a bit of small-scale
automation for proving theorems. The standard library introduces the
tactic `decide`

that uses the `Decidable`

instance to solve simple goals.

```
example : 10 < 5 ∨ 1 > 0 := by
decide
example : ¬ (True ∧ False) := by
decide
example : 10 * 20 = 200 := by
decide
theorem ex : True ∧ 2 = 1+1 := by
decide
#print ex
-- theorem ex : True ∧ 2 = 1 + 1 :=
-- of_decide_eq_true (Eq.refl true)
#check @of_decide_eq_true
-- ∀ {p : Prop} [Decidable p], decide p = true → p
#check @decide
-- (p : Prop) → [Decidable p] → Bool
```

They work as follows. The expression `decide p`

tries to infer a
decision procedure for `p`

, and, if it is successful, evaluates to
either `true`

or `false`

. In particular, if `p`

is a true closed
expression, `decide p`

will reduce definitionally to the Boolean `true`

.
On the assumption that `decide p = true`

holds, `of_decide_eq_true`

produces a proof of `p`

. The tactic `decide`

puts it all together to
prove a target `p`

. By the previous observations,
`decide`

will succeed any time the inferred decision procedure
for `c`

has enough information to evaluate, definitionally, to the `isTrue`

case.

## Managing Type Class Inference

If you are ever in a situation where you need to supply an expression
that Lean can infer by type class inference, you can ask Lean to carry
out the inference using `inferInstance`

:

```
def foo : Add Nat := inferInstance
def bar : Inhabited (Nat → Nat) := inferInstance
#check @inferInstance
-- {α : Sort u} → [α] → α
```

In fact, you can use Lean's `(t : T)`

notation to specify the class whose instance you are looking for,
in a concise manner:

```
#check (inferInstance : Add Nat)
```

You can also use the auxiliary definition `inferInstanceAs`

:

```
#check inferInstanceAs (Add Nat)
#check @inferInstanceAs
-- (α : Sort u) → [α] → α
```

Sometimes Lean can't find an instance because the class is buried
under a definition. For example, Lean cannot
find an instance of `Inhabited (Set α)`

. We can declare one
explicitly:

```
def Set (α : Type u) := α → Prop
-- fails
-- example : Inhabited (Set α) :=
-- inferInstance
instance : Inhabited (Set α) :=
inferInstanceAs (Inhabited (α → Prop))
```

At times, you may find that the type class inference fails to find an expected instance, or, worse, falls into an infinite loop and times out. To help debug in these situations, Lean enables you to request a trace of the search:

```
set_option trace.Meta.synthInstance true
```

If you are using VS Code, you can read the results by hovering over
the relevant theorem or definition, or opening the messages window
with `Ctrl-Shift-Enter`

. In Emacs, you can use `C-c C-x`

to run an
independent Lean process on your file, and the output buffer will show
a trace every time the type class resolution procedure is subsequently
triggered.

You can also limit the search using the following options:

```
set_option synthInstance.maxHeartbeats 10000
set_option synthInstance.maxSize 400
```

Option `synthInstance.maxHeartbeats`

specifies the maximum amount of
heartbeats per typeclass resolution problem. A heartbeat is the number of
(small) memory allocations (in thousands), 0 means there is no limit.
Option `synthInstance.maxSize`

is the maximum number of instances used
to construct a solution in the type class instance synthesis procedure.

Remember also that in both the VS Code and Emacs editor modes, tab
completion works in `set_option`

, to help you find suitable options.

As noted above, the type class instances in a given context represent a Prolog-like program, which gives rise to a backtracking search. Both the efficiency of the program and the solutions that are found can depend on the order in which the system tries the instance. Instances which are declared last are tried first. Moreover, if instances are declared in other modules, the order in which they are tried depends on the order in which namespaces are opened. Instances declared in namespaces which are opened later are tried earlier.

You can change the order that type class instances are tried by
assigning them a *priority*. When an instance is declared, it is
assigned a default priority value. You can assign other priorities
when defining an instance. The following example illustrates how this
is done:

```
class Foo where
a : Nat
b : Nat
instance (priority := default+1) i1 : Foo where
a := 1
b := 1
instance i2 : Foo where
a := 2
b := 2
example : Foo.a = 1 :=
rfl
instance (priority := default+2) i3 : Foo where
a := 3
b := 3
example : Foo.a = 3 :=
rfl
```

## Coercions using Type Classes

The most basic type of coercion maps elements of one type to another. For example, a coercion from `Nat`

to `Int`

allows us to view any element `n : Nat`

as an element of `Int`

. But some coercions depend on parameters; for example, for any type `α`

, we can view any element `as : List α`

as an element of `Set α`

, namely, the set of elements occurring in the list. The corresponding coercion is defined on the "family" of types `List α`

, parameterized by `α`

.

Lean allows us to declare three kinds of coercions:

- from a family of types to another family of types
- from a family of types to the class of sorts
- from a family of types to the class of function types

The first kind of coercion allows us to view any element of a member of the source family as an element of a corresponding member of the target family. The second kind of coercion allows us to view any element of a member of the source family as a type. The third kind of coercion allows us to view any element of the source family as a function. Let us consider each of these in turn.

In Lean, coercions are implemented on top of the type class resolution framework. We define a coercion from `α`

to `β`

by declaring an instance of `Coe α β`

. For example, we can define a coercion from `Bool`

to `Prop`

as follows:

```
instance : Coe Bool Prop where
coe b := b = true
```

This enables us to use boolean terms in if-then-else expressions:

```
#eval if true then 5 else 3
#eval if false then 5 else 3
```

We can define a coercion from `List α`

to `Set α`

as follows:

```
def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
| [] => Set.empty
| a::as => {a} ∪ as.toSet
instance : Coe (List α) (Set α) where
coe a := a.toSet
def s : Set Nat := {1}
#check s ∪ [2, 3]
-- s ∪ List.toSet [2, 3] : Set Nat
```

We can use the notation `↑`

to force a coercion to be introduced in a particular place. It is also helpful to make our intent clear, and work around limitations of the coercion resolution system.

```
def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
| [] => Set.empty
| a::as => {a} ∪ as.toSet
instance : Coe (List α) (Set α) where
coe a := a.toSet
def s : Set Nat := {1}
#check let x := ↑[2, 3]; s ∪ x
-- let x := List.toSet [2, 3]; s ∪ x : Set Nat
#check let x := [2, 3]; s ∪ x
-- let x := [2, 3]; s ∪ List.toSet x : Set Nat
```

Lean also supports dependent coercions using the type class `CoeDep`

. For example, we cannot coerce arbitrary propositions to `Bool`

, only the ones that implement the `Decidable`

typeclass.

```
instance (p : Prop) [Decidable p] : CoeDep Prop p Bool where
coe := decide p
```

Lean will also chain (non-dependent) coercions as necessary. Actually, the type class `CoeT`

is the transitive closure of `Coe`

.

Let us now consider the second kind of coercion. By the *class of sorts*, we mean the collection of universes `Type u`

. A coercion of the second kind is of the form:

```
c : (x1 : A1) → ... → (xn : An) → F x1 ... xn → Type u
```

where `F`

is a family of types as above. This allows us to write `s : t`

whenever `t`

is of type `F a1 ... an`

. In other words, the coercion allows us to view the elements of `F a1 ... an`

as types. This is very useful when defining algebraic structures in which one component, the carrier of the structure, is a `Type`

. For example, we can define a semigroup as follows:

```
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
```

In other words, a semigroup consists of a type, `carrier`

, and a multiplication, `mul`

, with the property that the multiplication is associative. The `instance`

command allows us to write `a * b`

instead of `Semigroup.mul S a b`

whenever we have `a b : S.carrier`

; notice that Lean can infer the argument `S`

from the types of `a`

and `b`

. The function `Semigroup.carrier`

maps the class `Semigroup`

to the sort `Type u`

:

```
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
#check Semigroup.carrier
```

If we declare this function to be a coercion, then whenever we have a semigroup `S : Semigroup`

, we can write `a : S`

instead of `a : S.carrier`

:

```
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
example (S : Semigroup) (a b c : S) : (a * b) * c = a * (b * c) :=
Semigroup.mul_assoc _ a b c
```

It is the coercion that makes it possible to write `(a b c : S)`

. Note that, we define an instance of `CoeSort Semigroup (Type u)`

instead of `Coe Semigroup (Type u)`

.

By the *class of function types*, we mean the collection of Pi types `(z : B) → C`

. The third kind of coercion has the form:

```
c : (x1 : A1) → ... → (xn : An) → (y : F x1 ... xn) → (z : B) → C
```

where `F`

is again a family of types and `B`

and `C`

can depend on `x1, ..., xn, y`

. This makes it possible to write `t s`

whenever `t`

is an element of `F a1 ... an`

. In other words, the coercion enables us to view elements of `F a1 ... an`

as functions. Continuing the example above, we can define the notion of a morphism between semigroups `S1`

and `S2`

. That is, a function from the carrier of `S1`

to the carrier of `S2`

(note the implicit coercion) that respects the multiplication. The projection `morphism.mor`

takes a morphism to the underlying function:

```
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
structure Morphism (S1 S2 : Semigroup) where
mor : S1 → S2
resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)
#check @Morphism.mor
```

As a result, it is a prime candidate for the third type of coercion.

```
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
structure Morphism (S1 S2 : Semigroup) where
mor : S1 → S2
resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)
instance (S1 S2 : Semigroup) : CoeFun (Morphism S1 S2) (fun _ => S1 → S2) where
coe m := m.mor
theorem resp_mul {S1 S2 : Semigroup} (f : Morphism S1 S2) (a b : S1)
: f (a * b) = f a * f b :=
f.resp_mul a b
example (S1 S2 : Semigroup) (f : Morphism S1 S2) (a : S1) :
f (a * a * a) = f a * f a * f a :=
calc f (a * a * a)
_ = f (a * a) * f a := by rw [resp_mul f]
_ = f a * f a * f a := by rw [resp_mul f]
```

With the coercion in place, we can write `f (a * a * a)`

instead of `f.mor (a * a * a)`

. When the `Morphism`

, `f`

, is used where a function is expected, Lean inserts the coercion. Similar to `CoeSort`

, we have yet another class `CoeFun`

for this class of coercions. The field `F`

is used to specify the function type we are coercing to. This type may depend on the type we are coercing from.