Type Classes and Polymorphism

It can be useful to write functions that work for any overloading of a given function. For instance, IO.println works for any type that has an instance of ToString. This is indicated using square brackets around the required instance: the type of IO.println is {α : Type} → [ToString α] → α → IO Unit. This type says that IO.println accepts an argument of type α, which Lean should determine automatically, and that there must be a ToString instance available for α. It returns an IO action.

Checking Polymorphic Functions' Types

Checking the type of a function that takes implicit arguments or uses type classes requires the use of some additional syntax. Simply writing

#check (IO.println)

yields a type with metavariables:

IO.println : ?m.3620 → IO Unit

This is because Lean does its best to discover implicit arguments, and the presence of metavariables indicates that it did not yet discover enough type information to do so. To understand the signature of a function, this feature can be suppressed with an at-sign (@) before the function's name:

#check @IO.println

@IO.println : {α : Type u_1} → [inst : ToString α] → α → IO Unit

In this output, the instance itself has been given the name inst. Additionally, there is a u_1 after Type, which uses a feature of Lean that has not yet been introduced. For now, ignore these parameters to Type.

Defining Polymorphic Functions with Instance Implicits

A function that sums all entries in a list needs two instances: Add allows the entries to be added, and an OfNat instance for 0 provides a sensible value to return for the empty list:

def List.sum [Add α] [OfNat α 0] : List α → α
  | [] => 0
  | x :: xs => x + xs.sum

This function can be used for a list of Nats:

def fourNats : List Nat := [1, 2, 3, 4]

#eval fourNats.sum

but not for a list of Pos numbers:

def fourPos : List Pos := [1, 2, 3, 4]

#eval fourPos.sum

failed to synthesize instance
  OfNat Pos 0

Specifications of required instances in square brackets are called instance implicits. Behind the scenes, every type class defines a structure that has a field for each overloaded operation. Instances are values of that structure type, with each field containing an implementation. At a call site, Lean is responsible for finding an instance value to pass for each instance implicit argument. The most important difference between ordinary implicit arguments and instance implicits is the strategy that Lean uses to find an argument value. In the case of ordinary implicit arguments, Lean uses a technique called unification to find a single unique argument value that would allow the program to pass the type checker. This process relies only on the specific types involved in the function's definition and the call site. For instance implicits, Lean instead consults a built-in table of instance values.

Just as the OfNat instance for Pos took a natural number n as an automatic implicit argument, instances may also take instance implicit arguments themselves. The section on polymorphism presented a polymorphic point type:

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

Addition of points should add the underlying x and y fields. Thus, an Add instance for PPoint requires an Add instance for whatever type these fields have. In other words, the Add instance for PPoint requires a further Add instance for α:

instance [Add α] : Add (PPoint α) where
  add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }

When Lean encounters an addition of two points, it searches for and finds this instance. It then performs a further search for the Add α instance.

The instance values that are constructed in this way are values of the type class's structure type. A successful recursive instance search results in a structure value that has a reference to another structure value. An instance of Add (PPoint Nat) contains a reference to the instance of Add Nat that was found.

This recursive search process means that type classes offer significantly more power than plain overloaded functions. A library of polymorphic instances is a set of code building blocks that the compiler will assemble on its own, given nothing but the desired type. Polymorphic functions that take instance arguments are latent requests to the type class mechanism to assemble helper functions behind the scenes. The API's clients are freed from the burden of plumbing together all of the necessary parts by hand.

Methods and Implicit Arguments

The type of @OfNat.ofNat may be surprising. It is {α : Type} → (n : Nat) → [OfNat α n] → α, in which the Nat argument n occurs as an explicit function argument. In the declaration of the method, however, ofNat simply has type α. This seeming discrepancy is because declaring a type class really results in the following:

A structure type to contain the implementation of each overloaded operation
A namespace with the same name as the class
For each method, a function in the class's namespace that retrieves its implementation from an instance

This is analogous to the way that declaring a new structure also declares accessor functions. The primary difference is that a structure's accessors take the structure value as an explicit argument, while the type class methods take the instance value as an instance implicit to be found automatically by Lean.

In order for Lean to find an instance, its arguments must be available. This means that each argument to the type class must be an argument to the method that occurs before the instance. It is most convenient when these arguments are implicit, because Lean does the work of discovering their values. For example, @Add.add has the type {α : Type} → [Add α] → α → α → α. In this case, the type argument α can be implicit because the arguments to Add.add provide information about which type the user intended. This type can then be used to search for the Add instance.

In the case of ofNat, however, the particular Nat literal to be decoded does not appear as part of any other argument. This means that Lean would have no information to use when attempting to figure out the implicit argument n. The result would be a very inconvenient API. Thus, in these cases, Lean uses an explicit argument for the class's method.

Functional Programming in Lean

Type Classes and Polymorphism

Checking Polymorphic Functions' Types

Defining Polymorphic Functions with Instance Implicits

Methods and Implicit Arguments

Exercises

Even Number Literals

Recursive Instance Search Depth