Coercions

In mathematics, it is common to use the same symbol to stand for different aspects of some object in different contexts. For example, if a ring is referred to in a context where a set is expected, then it is understood that the ring's underlying set is what's intended. In programming languages, it is common to have rules to automatically translate values of one type into values of another type. For instance, Java allows a byte to be automatically promoted to an int, and Kotlin allows a non-nullable type to be used in a context that expects a nullable version of the type.

In Lean, both purposes are served by a mechanism called coercions. When Lean encounters an expression of one type in a context that expects a different type, it will attempt to coerce the expression before reporting a type error. Unlike Java, C, and Kotlin, the coercions are extensible by defining instances of type classes.

Positive Numbers

For example, every positive number corresponds to a natural number. The function Pos.toNat that was defined earlier converts a Pos to the corresponding Nat:

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

The function List.drop, with type {α : Type} → Nat → List α → List α, removes a prefix of a list. Applying List.drop to a Pos, however, leads to a type error:

[1, 2, 3, 4].drop (2 : Pos)

application type mismatch
  List.drop 2
argument
  2
has type
  Pos : Type
but is expected to have type
  Nat : Type

Because the author of List.drop did not make it a method of a type class, it can't be overridden by defining a new instance.

The type class Coe describes overloaded ways of coercing from one type to another:

class Coe (α : Type) (β : Type) where
  coe : α → β

An instance of Coe Pos Nat is enough to allow the prior code to work:

instance : Coe Pos Nat where
  coe x := x.toNat

#eval [1, 2, 3, 4].drop (2 : Pos)

[3, 4]

Using #check shows the result of the instance search that was used behind the scenes:

#check [1, 2, 3, 4].drop (2 : Pos)

List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat

Chaining Coercions

When searching for coercions, Lean will attempt to assemble a coercion out of a chain of smaller coercions. For example, there is already a coercion from Nat to Int. Because of that instance, combined with the Coe Pos Nat instance, the following code is accepted:

def oneInt : Int := Pos.one

This definition uses two coercions: from Pos to Nat, and then from Nat to Int.

The Lean compiler does not get stuck in the presence of circular coercions. For example, even if two types A and B can be coerced to one another, their mutual coercions can be used to find a path:

inductive A where
  | a

inductive B where
  | b

instance : Coe A B where
  coe _ := B.b

instance : Coe B A where
  coe _ := A.a

instance : Coe Unit A where
  coe _ := A.a

def coercedToB : B := ()

Remember: the double parentheses () is short for the constructor Unit.unit. After deriving a Repr B instance,

#eval coercedToB

results in:

B.b

The Option type can be used similarly to nullable types in C# and Kotlin: the none constructor represents the absence of a value. The Lean standard library defines a coercion from any type α to Option α that wraps the value in some. This allows option types to be used in a manner even more similar to nullable types, because some can be omitted. For instance, the function List.getLast? that finds the last entry in a list can be written without a some around the return value x:

def List.last? : List α → Option α
  | [] => none
  | [x] => x
  | _ :: x :: xs => last? (x :: xs)

Instance search finds the coercion, and inserts a call to coe, which wraps the argument in some. These coercions can be chained, so that nested uses of Option don't require nested some constructors:

def perhapsPerhapsPerhaps : Option (Option (Option String)) :=
  "Please don't tell me"

Coercions are only activated automatically when Lean encounters a mismatch between an inferred type and a type that is imposed from the rest of the program. In cases with other errors, coercions are not activated. For example, if the error is that an instance is missing, coercions will not be used:

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

This can be worked around by manually indicating the desired type to be used for OfNat:

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  (392 : Nat)

Additionally, coercions can be manually inserted using an up arrow:

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  ↑(392 : Nat)

In some cases, this can be used to ensure that Lean finds the right instances. It can also make the programmer's intentions more clear.

Non-Empty Lists and Dependent Coercions

An instance of Coe α β makes sense when the type β has a value that can represent each value from the type α. Coercing from Nat to Int makes sense, because the type Int contains all the natural numbers. Similarly, a coercion from non-empty lists to ordinary lists makes sense because the List type can represent every non-empty list:

instance : Coe (NonEmptyList α) (List α) where
  coe
    | { head := x, tail := xs } => x :: xs

This allows non-empty lists to be used with the entire List API.

On the other hand, it is impossible to write an instance of Coe (List α) (NonEmptyList α), because there's no non-empty list that can represent the empty list. This limitation can be worked around by using another version of coercions, which are called dependent coercions. Dependent coercions can be used when the ability to coerce from one type to another depends on which particular value is being coerced. Just as the OfNat type class takes the particular Nat being overloaded as a parameter, dependent coercion takes the value being coerced as a parameter:

class CoeDep (α : Type) (x : α) (β : Type) where
  coe : β

This is a chance to select only certain values, either by imposing further type class constraints on the value or by writing certain constructors directly. For example, any List that is not actually empty can be coerced to a NonEmptyList:

instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := { head := x, tail := xs }

Coercing to Types

In mathematics, it is common to have a concept that consists of a set equipped with additional structure. For example, a monoid is some set S, an element s of S, and an associative binary operator on S, such that s is neutral on the left and right of the operator. S is referred to as the "carrier set" of the monoid. The natural numbers with zero and addition form a monoid, because addition is associative and adding zero to any number is the identity. Similarly, the natural numbers with one and multiplication also form a monoid. Monoids are also widely used in functional programming: lists, the empty list, and the append operator form a monoid, as do strings, the empty string, and string append:

structure Monoid where
  Carrier : Type
  neutral : Carrier
  op : Carrier → Carrier → Carrier

def natMulMonoid : Monoid :=
  { Carrier := Nat, neutral := 1, op := (· * ·) }

def natAddMonoid : Monoid :=
  { Carrier := Nat, neutral := 0, op := (· + ·) }

def stringMonoid : Monoid :=
  { Carrier := String, neutral := "", op := String.append }

def listMonoid (α : Type) : Monoid :=
  { Carrier := List α, neutral := [], op := List.append }

Given a monoid, it is possible to write the foldMap function that, in a single pass, transforms the entries in a list into a monoid's carrier set and then combines them using the monoid's operator. Because monoids have a neutral element, there is a natural result to return when the list is empty, and because the operator is associative, clients of the function don't have to care whether the recursive function combines elements from left to right or from right to left.

def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
  let rec go (soFar : M.Carrier) : List α → M.Carrier
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

Even though a monoid consists of three separate pieces of information, it is common to just refer to the monoid's name in order to refer to its set. Instead of saying "Let A be a monoid and let x and y be elements of its carrier set", it is common to say "Let A be a monoid and let x and y be elements of A". This practice can be encoded in Lean by defining a new kind of coercion, from the monoid to its carrier set.

The CoeSort class is just like the Coe class, with the exception that the target of the coercion must be a sort, namely Type or Prop. The term sort in Lean refers to these types that classify other types—Type classifies types that themselves classify data, and Prop classifies propositions that themselves classify evidence of their truth. Just as Coe is checked when a type mismatch occurs, CoeSort is used when something other than a sort is provided in a context where a sort would be expected.

The coercion from a monoid into its carrier set extracts the carrier:

instance : CoeSort Monoid Type where
  coe m := m.Carrier

With this coercion, the type signatures become less bureaucratic:

def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
  let rec go (soFar : M) : List α → M
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

Another useful example of CoeSort is used to bridge the gap between Bool and Prop. As discussed in the section on ordering and equality, Lean's if expression expects the condition to be a decidable proposition rather than a Bool. Programs typically need to be able to branch based on Boolean values, however. Rather than have two kinds of if expression, the Lean standard library defines a coercion from Bool to the proposition that the Bool in question is equal to true:

instance : CoeSort Bool Prop where
  coe b := b = true

In this case, the sort in question is Prop rather than Type.

Coercing to Functions

Many datatypes that occur regularly in programming consist of a function along with some extra information about it. For example, a function might be accompanied by a name to show in logs or by some configuration data. Additionally, putting a type in a field of a structure, similarly to the Monoid example, can make sense in contexts where there is more than one way to implement an operation and more manual control is needed than type classes would allow. For example, the specific details of values emitted by a JSON serializer may be important because another application expects a particular format. Sometimes, the function itself may be derivable from just the configuration data.

A type class called CoeFun can transform values from non-function types to function types. CoeFun has two parameters: the first is the type whose values should be transformed into functions, and the second is an output parameter that determines exactly which function type is being targeted.

class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where
  coe : (x : α) → makeFunctionType x

The second parameter is itself a function that computes a type. In Lean, types are first-class and can be passed to functions or returned from them, just like anything else.

For example, a function that adds a constant amount to its argument can be represented as a wrapper around the amount to add, rather than by defining an actual function:

structure Adder where
  howMuch : Nat

A function that adds five to its argument has a 5 in the howMuch field:

def add5 : Adder := ⟨5⟩

This Adder type is not a function, and applying it to an argument results in an error:

#eval add5 3

function expected at
  add5
term has type
  Adder

Defining a CoeFun instance causes Lean to transform the adder into a function with type Nat → Nat:

instance : CoeFun Adder (fun _ => Nat → Nat) where
  coe a := (· + a.howMuch)

#eval add5 3

8

Because all Adders should be transformed into Nat → Nat functions, the argument to CoeFun's second parameter was ignored.

When the value itself is needed to determine the right function type, then CoeFun's second parameter is no longer ignored. For example, given the following representation of JSON values:

inductive JSON where
  | true : JSON
  | false : JSON
  | null : JSON
  | string : String → JSON
  | number : Float → JSON
  | object : List (String × JSON) → JSON
  | array : List JSON → JSON
deriving Repr

a JSON serializer is a structure that tracks the type it knows how to serialize along with the serialization code itself:

structure Serializer where
  Contents : Type
  serialize : Contents → JSON

A serializer for strings need only wrap the provided string in the JSON.string constructor:

def Str : Serializer :=
  { Contents := String,
    serialize := JSON.string
  }

Viewing JSON serializers as functions that serialize their argument requires extracting the inner type of serializable data:

instance : CoeFun Serializer (fun s => s.Contents → JSON) where
  coe s := s.serialize

Given this instance, a serializer can be applied directly to an argument:

def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
  JSON.object [
    ("title", JSON.string title),
    ("status", JSON.number 200),
    ("record", R record)
  ]

The serializer can be passed directly to buildResponse:

#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"

JSON.object
  [("title", JSON.string "Functional Programming in Lean"),
   ("status", JSON.number 200.000000),
   ("record", JSON.string "Programming is fun!")]

Aside: JSON as a String

It can be a bit difficult to understand JSON when encoded as Lean objects. To help make sure that the serialized response was what was expected, it can be convenient to write a simple converter from JSON to String. The first step is to simplify the display of numbers. JSON doesn't distinguish between integers and floating point numbers, and the type Float is used to represent both. In Lean, Float.toString includes a number of trailing zeros:

#eval (5 : Float).toString

"5.000000"

The solution is to write a little function that cleans up the presentation by dropping all trailing zeros, followed by a trailing decimal point:

def dropDecimals (numString : String) : String :=
  if numString.contains '.' then
    let noTrailingZeros := numString.dropRightWhile (· == '0')
    noTrailingZeros.dropRightWhile (· == '.')
  else numString

With this definition, #eval dropDecimals (5 : Float).toString yields "5", and #eval dropDecimals (5.2 : Float).toString yields "5.2".

The next step is to define a helper function to append a list of strings with a separator in between them:

def String.separate (sep : String) (strings : List String) : String :=
  match strings with
  | [] => ""
  | x :: xs => String.join (x :: xs.map (sep ++ ·))

This function is useful to account for comma-separated elements in JSON arrays and objects. #eval ", ".separate ["1", "2"] yields "1, 2", #eval ", ".separate ["1"] yields "1", and #eval ", ".separate [] yields "".

Finally, a string escaping procedure is needed for JSON strings, so that the Lean string containing "Hello!" can be output as "\"Hello!\"". Fortunately, the Lean compiler contains an internal function for escaping JSON strings already, called Lean.Json.escape. To access this function, add import Lean to the beginning of your file.

The function that emits a string from a JSON value is declared partial because Lean cannot see that it terminates. This is because recursive calls to asString occur in functions that are being applied by List.map, and this pattern of recursion is complicated enough that Lean cannot see that the recursive calls are actually being performed on smaller values. In an application that just needs to produce JSON strings and doesn't need to mathematically reason about the process, having the function be partial is not likely to cause problems.

partial def JSON.asString (val : JSON) : String :=
  match val with
  | true => "true"
  | false => "false"
  | null => "null"
  | string s => "\"" ++ Lean.Json.escape s ++ "\""
  | number n => dropDecimals n.toString
  | object members =>
    let memberToString mem :=
      "\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
    "{" ++ ", ".separate (members.map memberToString) ++ "}"
  | array elements =>
    "[" ++ ", ".separate (elements.map asString) ++ "]"

With this definition, the output of serialization is easier to read:

#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString

"{\\"title\\": \\"Functional Programming in Lean\\", \\"status\\": 200, \\"record\\": \\"Programming is fun!\\"}"

Messages You May Meet

Natural number literals are overloaded with the OfNat type class. Because coercions fire in cases where types don't match, rather than in cases of missing instances, a missing OfNat instance for a type does not cause a coercion from Nat to be applied:

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

Design Considerations

Coercions are a powerful tool that should be used responsibly. On the one hand, they can allow an API to naturally follow the everyday rules of the domain being modeled. This can be the difference between a bureaucratic mess of manual conversion functions and a clear program. As Abelson and Sussman wrote in the preface to Structure and Interpretation of Computer Programs (MIT Press, 1996),

Programs must be written for people to read, and only incidentally for machines to execute.

Coercions, used wisely, are a valuable means of achieving readable code that can serve as the basis for communication with domain experts. APIs that rely heavily on coercions have a number of important limitations, however. Think carefully about these limitations before using coercions in your own libraries.

First off, coercions are only applied in contexts where enough type information is available for Lean to know all of the types involved, because there are no output parameters in the coercion type classes. This means that a return type annotation on a function can be the difference between a type error and a successfully applied coercion. For example, the coercion from non-empty lists to lists makes the following program work:

def lastSpider : Option String :=
  List.getLast? idahoSpiders

On the other hand, if the type annotation is omitted, then the result type is unknown, so Lean is unable to find the coercion:

def lastSpider :=
  List.getLast? idahoSpiders

application type mismatch
  List.getLast? idahoSpiders
argument
  idahoSpiders
has type
  NonEmptyList String : Type
but is expected to have type
  List ?m.34258 : Type

More generally, when a coercion is not applied for some reason, the user receives the original type error, which can make it difficult to debug chains of coercions.

Finally, coercions are not applied in the context of field accessor notation. This means that there is still an important difference between expressions that need to be coerced and those that don't, and this difference is visible to users of your API.