6. Type Classes🔗

An operation is polymorphic if it can be used with multiple types. In Lean, polymorphism comes in three varieties:

universe polymorphism, where the sorts in a definition can be instantiated in various ways,
functions that take types as (potentially implicit) parameters, allowing a single body of code to work with any type, and
ad-hoc polymorphism, implemented with type classes, in which operations to be overloaded may have different implementations for different types.

Because Lean does not allow case analysis of types, polymorphic functions implement operations that are uniform for any choice of type argument; for example, List.map does not suddenly compute differently depending on whether the input list contains Strings or Nats. Ad-hoc polymorphic operations are useful when there is no “uniform” way to implement an operation; the canonical use case is for overloading arithmetic operators so that they work with Nat, Int, Float, and any other type that has a sensible notion of addition. Ad-hoc polymorphism may also involve multiple types; looking up a value at a given index in a collection involves the collection type, the index type, and the type of member elements to be extracted. A type classType classes were first described in Philip Wadler and Stephen Blott, 1980. “How to make ad-hoc polymorphism less ad hoc”. In Proceedings of the 16th Symposium on Principles of Programming Languages. describes a collection of overloaded operations (called methods) together with the involved types.

Type classes are very flexible. Overloading may involve multiple types; operations like indexing into a data structure can be overloaded for a specific choice of data structure, index type, element type, and even a predicate that asserts the presence of the key in the structure. Due to Lean's expressive type system, overloading operations is not restricted only to types; type classes may be parameterized by ordinary values, by families of types, and even by predicates or propositions. All of these possibilities are used in practice:

Natural number literals: The OfNat type class is used to interpret natural number literals. Instances may depend not only on the type being instantiated, but also on the number literal itself.
Computational effects: Type classes such as Monad, whose parameter is a function from one type to another, are used to provide special syntax for programs with side effects. The “type” for which operations are overloaded is actually a type-level function, such as Option, IO, or Except.
Predicates and propositions: The Decidable type class allows a decision procedure for a proposition to be found automatically by Lean. This is used as the basis for termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false.if-expressions, which may branch on any decidable proposition.

While ordinary polymorphic definitions simply expect instantiation with arbitrary parameters, the operators overloaded with type classes are to be instantiated with instances that define the overloaded operation for some specific set of parameters. These instance-implicit parameters are indicated in square brackets. At invocation sites, Lean either synthesizes a suitable instance from the available candidates or signals an error. Because instances may themselves have instance parameters, this search process may be recursive and result in a final composite instance value that combines code from a variety of instances. Thus, type class instance synthesis is also a means of constructing programs in a type-directed manner.

Here are some typical use cases for type classes:

Type classes may represent overloaded operators, such as arithmetic that can be used with a variety of types of numbers or a membership predicate that can be used for a variety of data structures. There is often a single canonical choice of operator for a given type—after all, there is no sensible alternative definition of addition for Nat—but this is not an essential property, and libraries may provide alternative instances if needed.
Type classes can represent an algebraic structure, providing both the extra structure and the axioms required by the structure. For example, a type class that represents an Abelian group may contain methods for a binary operator, a unary inverse operator, an identity element, as well as proofs that the binary operator is associative and commutative, that the identity is an identity, and that the inverse operator yields the identity element on both sides of the operator. Here, there may not be a canonical choice of structure, and a library may provide many ways to instantiate a given set of axioms; there are two equally canonical monoid structures over the integers.
A type class can represent a relation between two types that allows them to be used together in some novel way by a library. The Coe class represents automatically-inserted coercions from one type to another, and MonadLift represents a way to run operations with one kind of effect in a context that expects another kind.
Type classes can represent a framework of type-driven code generation, where instances for polymorphic types each contribute some portion of a final program. The Repr class defines a canonical pretty printer for a type, and polymorphic types end up with polymorphic Repr instances. When pretty printing is finally invoked on an expression with a known concrete type, such as List (Nat × (String ⊕ Int)), the resulting pretty printer contains code assembled from the Repr instances for List, Prod, Nat, Sum, String, and Int.