# Standard Classes

This section presents a variety of operators and functions that can be overloaded using type classes in Lean.
Each operator or function corresponds to a method of a type class.
Unlike C++, infix operators in Lean are defined as abbreviations for named functions; this means that overloading them for new types is not done using the operator itself, but rather using the underlying name (such as `HAdd.hAdd`

).

## Arithmetic

Most arithmetic operators are available in a heterogeneous form, where the arguments may have different type and an output parameter decides the type of the resulting expression.
For each heterogeneous operator, there is a corresponding homogeneous version that can found by removing the letter `h`

, so that `HAdd.hAdd`

becomes `Add.add`

.
The following arithmetic operators are overloaded:

Expression | Desugaring | Class Name |
---|---|---|

`x + y` | `HAdd.hAdd x y` | `HAdd` |

`x - y` | `HSub.hSub x y` | `HSub` |

`x * y` | `HMul.hMul x y` | `HMul` |

`x / y` | `HDiv.hDiv x y` | `HDiv` |

`x % y` | `HMod.hMod x y` | `HMod` |

`x ^ y` | `HPow.hPow x y` | `HPow` |

`(- x)` | `Neg.neg x` | `Neg` |

## Bitwise Operators

Lean contains a number of standard bitwise operators that are overloaded using type classes.
There are instances for fixed-width types such as `UInt8`

, `UInt16`

, `UInt32`

, `UInt64`

, and `USize`

.
The latter is the size of words on the current platform, typically 32 or 64 bits.
The following bitwise operators are overloaded:

Expression | Desugaring | Class Name |
---|---|---|

`x &&& y` | `HAnd.hAnd x y` | `HAnd` |

`x ||| y ` | `HOr.hOr x y` | `HOr` |

`x ^^^ y` | `HXor.hXor x y` | `HXor` |

`~~~ x` | `Complement.complement x` | `Complement` |

`x >>> y` | `HShiftRight.hShiftRight x y` | `HShiftRight` |

`x <<< y` | `HShiftLeft.hShiftLeft x y` | `HShiftLeft` |

Because the names `And`

and `Or`

are already taken as the names of logical connectives, the homogeneous versions of `HAnd`

and `HOr`

are called `AndOp`

and `OrOp`

rather than `And`

and `Or`

.

## Equality and Ordering

Testing equality of two values typically uses the `BEq`

class, which is short for "Boolean equality".
Due to Lean's use as a theorem prover, there are really two kinds of equality operators in Lean:

*Boolean equality*is the same kind of equality that is found in other programming languages. It is a function that takes two values and returns a`Bool`

. Boolean equality is written with two equals signs, just as in Python and C#. Because Lean is a pure functional language, there's no separate notions of reference vs value equality—pointers cannot be observed directly.*Propositional equality*is the mathematical statement that two things are equal. Propositional equality is not a function; rather, it is a mathematical statement that admits proof. It is written with a single equals sign. A statement of propositional equality is like a type that classifies evidence of this equality.

Both notions of equality are important, and used for different purposes.
Boolean equality is useful in programs, when a decision needs to be made about whether two values are equal.
For example, `"Octopus" == "Cuttlefish"`

evaluates to `false`

, and `"Octopodes" == "Octo".append "podes"`

evaluates to `true`

.
Some values, such as functions, cannot be checked for equality.
For example, `(fun (x : Nat) => 1 + x) == (Nat.succ ·)`

yields the error:

```
failed to synthesize instance
BEq (Nat → Nat)
```

As this message indicates, `==`

is overloaded using a type class.
The expression `x == y`

is actually shorthand for `BEq.beq x y`

.

Propositional equality is a mathematical statement rather than an invocation of a program.
Because propositions are like types that describe evidence for some statement, propositional equality has more in common with types like `String`

and `Nat → List Int`

than it does with Boolean equality.
This means that it can't automatically be checked.
However, the equality of any two expressions can be stated in Lean, so long as they have the same type.
The statement `(fun (x : Nat) => 1 + x) = (Nat.succ ·)`

is a perfectly reasonable statement.
From the perspective of mathematics, two functions are equal if they map equal inputs to equal outputs, so this statement is even true, though it requires a two-line proof to convince Lean of this fact.

Generally speaking, when using Lean as a programming language, it's easiest to stick to Boolean functions rather than propositions.
However, as the names `true`

and `false`

for `Bool`

's constructors suggest, this difference is sometimes blurred.
Some propositions are *decidable*, which means that they can be checked just like a Boolean function.
The function that checks whether the proposition is true or false is called a *decision procedure*, and it returns *evidence* of the truth or falsity of the proposition.
Some examples of decidable propositions include equality and inequality of natural numbers, equality of strings, and "ands" and "ors" of propositions that are themselves decidable.

In Lean, `if`

works with decidable propositions.
For example, `2 < 4`

is a proposition:

```
#check 2 < 4
```

```
2 < 4 : Prop
```

Nonetheless, it is perfectly acceptable to write it as the condition in an `if`

.
For example, `if 2 < 4 then 1 else 2`

has type `Nat`

and evaluates to `1`

.

Not all propositions are decidable.
If they were, then computers would be able to prove any true proposition just by running the decision procedure, and mathematicians would be out of a job.
More specifically, decidable propositions have an instance of the `Decidable`

type class which has a method that is the decision procedure.
Trying to use a proposition that isn't decidable as if it were a `Bool`

results in a failure to find the `Decidable`

instance.
For example, `if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no"`

results in:

```
failed to synthesize instance
Decidable ((fun x => 1 + x) = fun x => Nat.succ x)
```

The following propositions, that are usually decidable, are overloaded with type classes:

Expression | Desugaring | Class Name |
---|---|---|

`x < y` | `LT.lt x y` | `LT` |

`x ≤ y` | `LE.le x y` | `LE` |

`x > y` | `LT.lt y x` | `LT` |

`x ≥ y` | `LE.le y x` | `LE` |

Because defining new propositions hasn't yet been demonstrated, it may be difficult to define new instances of `LT`

and `LE`

.

Additionally, comparing values using `<`

, `==`

, and `>`

can be inefficient.
Checking first whether one value is less than another, and then whether they are equal, can require two traversals over large data structures.
To solve this problem, Java and C# have standard `compareTo`

and `CompareTo`

methods (respectively) that can be overridden by a class in order to implement all three operations at the same time.
These methods return a negative integer if the receiver is less than the argument, zero if they are equal, and a positive integer if the receiver is greater than the argument.
Rather than overload the meaning of integers, Lean has a built-in inductive type that describes these three possibilities:

```
inductive Ordering where
| lt
| eq
| gt
```

The `Ord`

type class can be overloaded to produce these comparisons.
For `Pos`

, an implementation can be:

```
def Pos.comp : Pos → Pos → Ordering
| Pos.one, Pos.one => Ordering.eq
| Pos.one, Pos.succ _ => Ordering.lt
| Pos.succ _, Pos.one => Ordering.gt
| Pos.succ n, Pos.succ k => comp n k
instance : Ord Pos where
compare := Pos.comp
```

In situations where `compareTo`

would be the right approach in Java, use `Ord.compare`

in Lean.

## Hashing

Java and C# have `hashCode`

and `GetHashCode`

methods, respectively, that compute a hash of a value for use in data structures such as hash tables.
The Lean equivalent is a type class called `Hashable`

:

```
class Hashable (α : Type) where
hash : α → UInt64
```

If two values are considered equal according to a `BEq`

instance for their type, then they should have the same hashes.
In other words, if `x == y`

then `hash x == hash y`

.
If `x ≠ y`

, then `hash x`

won't necessarily differ from `hash y`

(after all, there are infinitely more `Nat`

values than there are `UInt64`

values), but data structures built on hashing will have better performance if unequal values are likely to have unequal hashes.
This is the same expectation as in Java and C#.

The standard library contains a function `mixHash`

with type `UInt64 → UInt64 → UInt64`

that can be used to combine hashes for different fields for a constructor.
A reasonable hash function for an inductive datatype can be written by assigning a unique number to each constructor, and then mixing that number with the hashes of each field.
For example, a `Hashable`

instance for `Pos`

can be written:

```
def hashPos : Pos → UInt64
| Pos.one => 0
| Pos.succ n => mixHash 1 (hashPos n)
instance : Hashable Pos where
hash := hashPos
```

`Hashable`

instances for polymorphic types can use recursive instance search.
Hashing a `NonEmptyList α`

is only possible when `α`

can be hashed:

```
instance [Hashable α] : Hashable (NonEmptyList α) where
hash xs := mixHash (hash xs.head) (hash xs.tail)
```

Binary trees use both recursion and recursive instance search in the implementations of `BEq`

and `Hashable`

:

```
inductive BinTree (α : Type) where
| leaf : BinTree α
| branch : BinTree α → α → BinTree α → BinTree α
def eqBinTree [BEq α] : BinTree α → BinTree α → Bool
| BinTree.leaf, BinTree.leaf =>
true
| BinTree.branch l x r, BinTree.branch l2 x2 r2 =>
x == x2 && eqBinTree l l2 && eqBinTree r r2
| _, _ =>
false
instance [BEq α] : BEq (BinTree α) where
beq := eqBinTree
def hashBinTree [Hashable α] : BinTree α → UInt64
| BinTree.leaf =>
0
| BinTree.branch left x right =>
mixHash 1 (mixHash (hashBinTree left) (mixHash (hash x) (hashBinTree right)))
instance [Hashable α] : Hashable (BinTree α) where
hash := hashBinTree
```

## Deriving Standard Classes

Instance of classes like `BEq`

and `Hashable`

are often quite tedious to implement by hand.
Lean includes a feature called *instance deriving* that allows the compiler to automatically construct well-behaved instances of many type classes.
In fact, the `deriving Repr`

phrase in the definition of `Point`

in the section on structures is an example of instance deriving.

Instances can be derived in two ways.
The first can be used when defining a structure or inductive type.
In this case, add `deriving`

to the end of the type declaration followed by the names of the classes for which instances should be derived.
For a type that is already defined, a standalone `deriving`

command can be used.
Write `deriving instance C1, C2, ... for T`

to derive instances of `C1, C2, ...`

for the type `T`

after the fact.

`BEq`

and `Hashable`

instances can be derived for `Pos`

and `NonEmptyList`

using a very small amount of code:

```
deriving instance BEq, Hashable for Pos
deriving instance BEq, Hashable, Repr for NonEmptyList
```

Instances can be derived for at least the following classes:

`Inhabited`

`BEq`

`Repr`

`Hashable`

`Ord`

In some cases, however, the derived `Ord`

instance may not produce precisely the ordering desired in an application.
When this is the case, it's fine to write an `Ord`

instance by hand.
The collection of classes for which instances can be derived can be extended by advanced users of Lean.

Aside from the clear advantages in programmer productivity and code readability, deriving instances also makes code easier to maintain, because the instances are updated as the definitions of types evolve. Changesets involving updates to datatypes are easier to read without line after line of formulaic modifications to equality tests and hash computation.

## Appending

Many datatypes have some sort of append operator.
In Lean, appending two values is overloaded with the type class `HAppend`

, which is a heterogeneous operation like that used for arithmetic operations:

```
class HAppend (α : Type) (β : Type) (γ : outParam Type) where
hAppend : α → β → γ
```

The syntax `xs ++ ys`

desugars to `HAppend.hAppend xs ys`

.
For homogeneous cases, it's enough to implement an instance of `Append`

, which follows the usual pattern:

```
instance : Append (NonEmptyList α) where
append xs ys :=
{ head := xs.head, tail := xs.tail ++ ys.head :: ys.tail }
```

After defining the above instance,

```
#eval idahoSpiders ++ idahoSpiders
```

has the following output:

```
{ head := "Banded Garden Spider",
tail := ["Long-legged Sac Spider",
"Wolf Spider",
"Hobo Spider",
"Cat-faced Spider",
"Banded Garden Spider",
"Long-legged Sac Spider",
"Wolf Spider",
"Hobo Spider",
"Cat-faced Spider"] }
```

Similarly, a definition of `HAppend`

allows non-empty lists to be appended to ordinary lists:

```
instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
hAppend xs ys :=
{ head := xs.head, tail := xs.tail ++ ys }
```

With this instance available,

```
#eval idahoSpiders ++ ["Trapdoor Spider"]
```

results in

```
{ head := "Banded Garden Spider",
tail := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced Spider", "Trapdoor Spider"] }
```

## Functors

A polymorphic type is a *functor* if it has an overload for a function named `map`

that transforms every element contained in it by a function.
While most languages use this terminology, C#'s equivalent to `map`

is called `System.Linq.Enumerable.Select`

.
For example, mapping a function over a list constructs a new list in which each entry from the starting list has been replaced by the result of the function on that entry.
Mapping a function `f`

over an `Option`

leaves `none`

untouched, and replaces `some x`

with `some (f x)`

.

Here are some examples of functors and how their `Functor`

instances overload `map`

:

`Functor.map (· + 5) [1, 2, 3]`

evaluates to`[6, 7, 8]`

`Functor.map toString (some (List.cons 5 List.nil))`

evaluates to`some "[5]"`

`Functor.map List.reverse [[1, 2, 3], [4, 5, 6]]`

evaluates to`[[3, 2, 1], [6, 5, 4]]`

Because `Functor.map`

is a bit of a long name for this common operation, Lean also provides an infix operator for mapping a function, namely `<$>`

.
The prior examples can be rewritten as follows:

`(· + 5) <$> [1, 2, 3]`

evaluates to`[6, 7, 8]`

`toString <$> (some (List.cons 5 List.nil))`

evaluates to`some "[5]"`

`List.reverse <$> [[1, 2, 3], [4, 5, 6]]`

evaluates to`[[3, 2, 1], [6, 5, 4]]`

An instance of `Functor`

for `NonEmptyList`

requires specifying the `map`

function.

```
instance : Functor NonEmptyList where
map f xs := { head := f xs.head, tail := f <$> xs.tail }
```

Here, `map`

uses the `Functor`

instance for `List`

to map the function over the tail.
This instance is defined for `NonEmptyList`

rather than for `NonEmptyList α`

because the argument type `α`

plays no role in resolving the type class.
A `NonEmptyList`

can have a function mapped over it *no matter what the type of entries is*.
If `α`

were a parameter to the class, then it would be possible to make versions of `Functor`

that only worked for `NonEmptyList Nat`

, but part of being a functor is that `map`

works for any entry type.

Here is an instance of `Functor`

for `PPoint`

:

```
instance : Functor PPoint where
map f p := { x := f p.x, y := f p.y }
```

In this case, `f`

has been applied to both `x`

and `y`

.

Even when the type contained in a functor is itself a functor, mapping a function only goes down one layer.
That is, when using `map`

on a `NonEmptyList (PPoint Nat)`

, the function being mapped should take `PPoint Nat`

as its argument rather than `Nat`

.

The definition of the `Functor`

class uses one more language feature that has not yet been discussed: default method definitions.
Normally, a class will specify some minimal set of overloadable operations that make sense together, and then use polymorphic functions with instance implicit arguments that build on the overloaded operations to provide a larger library of features.
For example, the function `concat`

can concatenate any non-empty list whose entries are appendable:

```
def concat [Append α] (xs : NonEmptyList α) : α :=
let rec catList (start : α) : List α → α
| [] => start
| (z :: zs) => catList (start ++ z) zs
catList xs.head xs.tail
```

However, for some classes, there are operations that can be more efficiently implemented with knowledge of the internals of a datatype.

In these cases, a default method definition can be provided.
A default method definition provides a default implementation of a method in terms of the other methods.
However, instance implementors may choose to override this default with something more efficient.
Default method definitions contain `:=`

in a `class`

definition.

In the case of `Functor`

, some types have a more efficient way of implementing `map`

when the function being mapped ignores its argument.
Functions that ignore their arguments are called *constant functions* because they always return the same value.
Here is the definition of `Functor`

, in which `mapConst`

has a default implementation:

```
class Functor (f : Type → Type) where
map : {α β : Type} → (α → β) → f α → f β
mapConst {α β : Type} (x : α) (coll : f β) : f α :=
map (fun _ => x) coll
```

Just as a `Hashable`

instance that doesn't respect `BEq`

is buggy, a `Functor`

instance that moves around the data as it maps the function is also buggy.
For example, a buggy `Functor`

instance for `List`

might throw away its argument and always return the empty list, or it might reverse the list.
A bad instance for `PPoint`

might place `f x`

in both the `x`

and the `y`

fields.
Specifically, `Functor`

instances should follow two rules:

- Mapping the identity function should result in the original argument.
- Mapping two composed functions should have the same effect as composing their mapping.

More formally, the first rule says that `id <$> x`

equals `x`

.
The second rule says that `map (fun y => f (g y)) x`

equals `map f (map g x)`

.
The composition `fun y => f (g y)`

can also be written `f ∘ g`

.
These rules prevent implementations of `map`

that move the data around or delete some of it.

## Messages You May Meet

Lean is not able to derive instances for all classes. For example, the code

```
deriving instance ToString for NonEmptyList
```

results in the following error:

```
default handlers have not been implemented yet, class: 'ToString' types: [NonEmptyList]
```

Invoking `deriving instance`

causes Lean to consult an internal table of code generators for type class instances.
If the code generator is found, then it is invoked on the provided type to create the instance.
This message, however, means that no code generator was found for `ToString`

.

## Exercises

- Write an instance of
`HAppend (List α) (NonEmptyList α) (NonEmptyList α)`

and test it. - Implement a
`Functor`

instance for the binary tree datatype.