Coercions

Sometimes you have a term of a type, and you really want it to have another type (because that’s what we do in maths; we are liberal with our types, unlike Lean). For example you might have a natural number n : ℕ but a function f : ℝ → ℝ (like real.sqrt or similar), and you want to consider f n. This is problematic in a strongly typed language like Lean: n has type nat and not real, so f n does not make sense. However, if you try it…

import data.real.sqrt

def a : ℕ := 37

#check real.sqrt a -- real.sqrt ↑a : ℝ

…it works anyway! But actually looking more closely, something funny is going on; what is that ↑ by the a? That up-arrow is Lean’s notation for the completely obvious function from ℕ to ℝ which doesn’t have a name in mathematics but which Lean needs to apply in order for everything to typecheck.

So where did this coercion come from, what other types of coercions are there, and how do we make them?

Making coercions

Coercions are handled by Lean’s type class inference system. There are three kinds. You can coerce a term into a term (this is how a natural number becomes a real number), you can coerce a term into a type (this is how a subgroup becomes a group; remember that subgroups are terms of type subgroup G and in particular they’re terms; if we want to treat them as groups then they need to be promoted to types); and finally there is a special coercion which turns a term into a function.

Coercion from terms to terms

An example of this is coe_subtype. If X : Type is a type, and p : X → Prop is a predicate on X, then one can make a subtype of X consisting of the terms x : X such that p x is true. The notation for this subtype is {x : X // p x}. Remember that in type theory, this subtype is not a “subset” of X; a term of type {x : X // p x} is a pair consisting of a term x : X and a proof of p x. But given such a term, we might well want to treat it as a term of type X anyway. Here is some code indicating how this happens automatically:

variables (X : Type) (p : X → Prop) (s : {x : X // p x})

#check (s : X) -- ↑s : X

The reason this happens is because of the term coe_subtype : has_coe {x : X // p x} X which is defined in core Lean and which is tagged with the @[instance] attribute. The has_coe structure just has one field, namely the function from {x : X // p x} to X, which of course just returns the term of type X and throws away the proof. The type class system then takes care of everything after that; if Lean sees a term of type {x : X // p x} where it expects a term of type X then it magically applies this function and denotes the function itself with the up-arrow notation.

Coercions from terms to types

A subgroup of a group in Lean is a term, not a type. A subgroup H of G is a term of type subgroup G. In particular, H isn’t a type. So the below code shouldn’t work – but it does.

import tactic
import group_theory.subgroup.basic -- group theory

variables (G : Type) [group G] (H : subgroup G)
variable (x : H) -- shouldn't work because H isn't a type

#check x -- x : ↥H

Lean promotes the term H to a type, because of a term of type has_coe_to_sort (subgroup G) Type in the typeclass inference system. Coercions to types like this have a different notation than coercions from terms to terms; a different up-arrow ↥ is used. Type it with \u-|.

Coercions from terms to functions

A group homomorphism is a term of type G →* H in Lean, and to give a group homomorphism is to give a function plus some proofs. In particular, a group homomorphism is not actually a function, it is a tuple consisting of a function and some proofs. But of course we’d like to regard a group homomorphism as a function, and we can, because of the third type of coercion which Lean has, triggered by terms of type has_coe_to_fun.

import group_theory.subgroup.basic

variables (G H : Type) [group G] [group H] (f : G →* H) (x : G)

#check f x -- ⇑f x : H

Even though f isn’t strictly speaking a function (it’s a function plus some other stuff), Lean will still let us write f x, and it will interpret f as the function ⇑f : G → H. Here ⇑, which you can get with \u=, is the function from G →* H to G → H which the typeclass inference system produced for us, from the instance monoid_hom.has_coe_to_fun : has_coe_to_fun (M →* N) (λ _, M → N).