12.1. Coercion Insertion
The process of searching for a coercion from one type to another is called coercion insertion. Coercion insertion is attempted in the following situations where an error would otherwise occur:
-
The expected type for a term is not equal to the type found for the term.
-
A type or proposition is expected, but the term's type is not a universe.
-
A term is applied as though it were a function, but its type is not a function type.
Coercions are also inserted when they are explicitly requested. Each situation in which coercions may be inserted has a corresponding prefix operator that triggers the appropriate insertion.
Because coercions are inserted automatically, nested type ascriptions provide a way to precisely control the types involved in a coercion.
If α and β are not the same type, ((e : α) : β) arranges for e to have type α and then inserts a coercion from α to β.
When a coercion is discovered, the instances used to find it are unfolded and removed from the resulting term.
To the extent possible, calls to Coe.coe and related functions do not occur in the final term.
This process of unfolding makes terms more readable.
Even more importantly, it means that coercions can control the evaluation of the coerced terms by wrapping them in functions.
Controlling Evaluation with Coercions
The structure Later represents a term that can be evaluated in the future, by calling the contained function.
structure Later (α : Type u) where
get : Unit → α
A coercion from any value to a later value is performed by creating a function that wraps it.
instance : CoeTail α (Later α) where
coe x := { get := fun () => x }
However, if coercion insertion resulted in an application of CoeTail.coe, then this coercion would not have the desired effect at runtime, because the coerced value would be evaluated and then saved in the function's closure.
Because coercion implementations are unfolded, this instance is nonetheless useful.
def tomorrow : Later String :=
(Nat.fold 10000
(init := "")
(fun _ _ s => s ++ "tomorrow") : String)
Printing the resulting definition shows that the computation is inside the function's body:
#print tomorrow
def tomorrow : Later String :=
{ get := fun x => Nat.fold 10000 (fun x x s => s ++ "tomorrow") "" }
Duplicate Evaluation in Coercions
Because the contents of Coe instances are unfolded during coercion insertion, coercions that use their argument more than once should be careful to ensure that evaluation occurs just once.
This can be done by using a helper function that is not part of the instance, or by using Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
let to evaluate the coerced term and then re-use its resulting value.
The structure Twice requires that both fields have the same value:
structure Twice (α : Type u) where
first : α
second : α
first_eq_second : first = second
One way to define a coercion from α to Twice α is with a helper function twice.
The coe attribute marks it as a coercion so it can be shown correctly in proof goals and error messages.
@[coe]
def twice (x : α) : Twice α where
first := x
second := x
first_eq_second := rfl
instance : Coe α (Twice α) := ⟨twice⟩
When the Coe instance is unfolded, the call to twice remains, which causes its argument to be evaluated before the body of the function is executed.
As a result, the Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
dbg_trace executes just once:
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
hello
{ first := 5, second := 5, first_eq_second := _ }
Inlining the helper into the Coe instance results in a term that duplicates the Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
dbg_trace:
instance : Coe α (Twice α) where
coe x := ⟨x, x, rfl⟩
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
hello hello
{ first := 5, second := 5, first_eq_second := _ }
Introducing an intermediate name for the result of the evaluation prevents the duplicated work:
instance : Coe α (Twice α) where
coe x := let y := x; ⟨y, y, rfl⟩
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
hello
{ first := 5, second := 5, first_eq_second := _ }