When the Lean elaborator is expecting one type but produces a term with a different type, it attempts to automatically insert a coercion, which is a specially designated function from the term's type to the expected type. Coercions make it possible to use specific types to represent data while interacting with APIs that expect less-informative types. They also allow mathematical developments to follow the usual practice of “punning”, where the same symbol is used to stand for both an algebraic structure and its carrier set, with the precise meaning determined by context.
Lean's standard library and metaprogramming APIs define many coercions. Some examples include:
An α may be used where an Option α is expected. The coercion wraps the value in some.
An α may be used where a Thunk α is expected. The coercion wraps the term in a function to delay its evaluation.
When one syntax category c1 embeds into another category c2, a coercion from TSyntax c1 to TSyntax c2 performs any necessary wrapping to construct a valid syntax tree.
Coercions are found using type class synthesis. The set of coercions can be extended by adding further instances of the appropriate type classes.
All of the following examples rely on coercions:
example (n : Nat) : Int := n
example (n : Fin k) : Nat := n
example (x : α) : Option α := x
def th (f : Int → String) (x : Nat) : Thunk String := f x
open Lean in
example (n : Ident) : Term := n
In the case of th, using Lean.Parser.Command.print : command#print demonstrates that evaluation of the function application is delayed until the thunk's value is requested:
#print th
def th : (Int → String) → Nat → Thunk String :=
fun f x => { fn := fun x_1 => f ↑x }
Coercions are not used to resolve generalized field notation: only the inferred type of the term is considered.
However, a type ascription can be used to trigger a coercion to the type that has the desired generalized field.
Coercions are also not used to resolve OfNat instances: even though there is a default instance for OfNat Nat, a coercion from Nat to α does not allow natural number literals to be used for α.
The name Nat.bdiv is not defined, but Int.bdiv exists.
The coercion from Nat to Int is not considered when looking up the field bdiv:
example (n : Nat) := n.bdiv 2
invalid field 'bdiv', the environment does not contain 'Nat.bdiv' n has type Nat
This is because coercions are only inserted when there is an expected type that differs from an inferred type, and generalized fields are resolved based on the inferred type of the term before the dot.
Coercions can be triggered by adding a type ascription, which additionally causes the inferred type of the entire ascription term to be Int, allowing the function Int.bdiv to be found.
example (n : Nat) := (n : Int).bdiv 2
OfNat
Bin is an inductive type that represents binary numbers.
inductive Bin where
| done
| zero : Bin → Bin
| one : Bin → Bin
def Bin.toString : Bin → String
| .done => ""
| .one b => b.toString ++ "1"
| .zero b => b.toString ++ "0"
instance : ToString Bin where
toString
| .done => "0"
| b => Bin.toString b
Binary numbers can be converted to natural numbers by repeatedly applying Bin.succ:
def Bin.succ (b : Bin) : Bin :=
match b with
| .done => Bin.done.one
| .zero b => .one b
| .one b => .zero b.succ
def Bin.ofNat (n : Nat) : Bin :=
match n with
| 0 => .done
| n + 1 => (Bin.ofNat n).succ
Even if Bin.ofNat is registered as a coercion, natural number literals cannot be used for Bin:
attribute [coe] Bin.ofNat
instance : Coe Nat Bin where
coe := Bin.ofNat
#eval (9 : Bin)
failed to synthesize OfNat Bin 9 numerals are polymorphic in Lean, but the numeral `9` cannot be used in a context where the expected type is Bin due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command.
This is because coercions are inserted in response to mismatched types, but a failure to synthesize an OfNat instance is not a type mismatch.
The coercion can be used in the definition of the OfNat Bin instance:
instance : OfNat Bin n where
ofNat := n
#eval (10 : Bin)
1010
Most new coercions can be defined by declaring an instance of the Coe type class and applying the coe attribute to the function that performs the coercion.
To enable more control over coercions or to enable them in more contexts, Lean provides further classes that can be implemented, described in the rest of this chapter.
Decimal numbers can be defined as arrays of digits.
structure Decimal where
digits : Array (Fin 10)
Adding a coercion allows them to be used in contexts that expect Nat, but also contexts that expect any type that Nat can be coerced to.
@[coe]
def Decimal.toNat (d : Decimal) : Nat :=
d.digits.foldl (init := 0) fun n d => n * 10 + d.val
instance : Coe Decimal Nat where
coe := Decimal.toNat
This can be demonstrated by treating a Decimal as an Int as well as a Nat:
def twoHundredThirteen : Decimal where
digits := #[2, 1, 3]
def one : Decimal where
digits := #[1]
#eval (one : Int) - (twoHundredThirteen : Nat)
-212
Coe.{u, v} (α : semiOutParam (Sort u))
(β : Sort v) : Sort (max (max 1 u) v)
Coe α β is the typeclass for coercions from α to β. It can be transitively
chained with other Coe instances, and coercion is automatically used when
x has type α but it is used in a context where β is expected.
You can use the ↑x operator to explicitly trigger coercion.
Coe.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).