Positive Numbers

In some applications, only positive numbers make sense. For example, compilers and interpreters typically use one-indexed line and column numbers for source positions, and a datatype that represents only non-empty lists will never report a length of zero. Rather than relying on natural numbers, and littering the code with assertions that the number is not zero, it can be useful to design a datatype that represents only positive numbers.

One way to represent positive numbers is very similar to Nat, except with one as the base case instead of zero:

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

This datatype represents exactly the intended set of values, but it is not very convenient to use. For example, numeric literals are rejected:

def seven : Pos := 7

failed to synthesize instance
  OfNat Pos 7

Instead, the constructors must be used directly:

def seven : Pos :=
  Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))

Similarly, addition and multiplication are not easy to use:

def fourteen : Pos := seven + seven

failed to synthesize instance
  HAdd Pos Pos ?m.291

def fortyNine : Pos := seven * seven

failed to synthesize instance
  HMul Pos Pos ?m.291

Each of these error messages begins with failed to synthesize instance. This indicates that the error is due to an overloaded operation that has not been implemented, and it describes the type class that must be implemented.

Classes and Instances

A type class consists of a name, some parameters, and a collection of methods. The parameters describe the types for which overloadable operations are being defined, and the methods are the names and type signatures of the overloadable operations. Once again, there is a terminology clash with object-oriented languages. In object-oriented programming, a method is essentially a function that is connected to a particular object in memory, with special access to the object's private state. Objects are interacted with via their methods. In Lean, the term "method" refers to an operation that has been declared to be overloadable, with no special connection to objects or values or private fields.

One way to overload addition is to define a type class named Plus, with an addition method named plus. Once an instance of Plus for Nat has been defined, it becomes possible to add two Nats using Plus.plus:

#eval Plus.plus 5 3

Adding more instances allows Plus.plus to take more types of arguments.

In the following type class declaration, Plus is the name of the class, α : Type is the only argument, and plus : α → α → α is the only method:

class Plus (α : Type) where
  plus : α → α → α

This declaration says that there is a type class Plus that overloads operations with respect to a type α. In particular, there is one overloaded operation called plus that takes two αs and returns an α.

Type classes are first class, just as types are first class. In particular, a type class is another kind of type. The type of Plus is Type → Type, because it takes a type as an argument (α) and results in a new type that describes the overloading of Plus's operation for α.

To overload plus for a particular type, write an instance:

instance : Plus Nat where
  plus := Nat.add

The colon after instance indicates that Plus Nat is indeed a type. Each method of class Plus should be assigned a value using :=. In this case, there is only one method: plus.

By default, type class methods are defined in a namespace with the same name as the type class. It can be convenient to open the namespace so that users don't need to type the name of the class first. Parentheses in an open command indicate that only the indicated names from the namespace are to be made accessible:

open Plus (plus)

#eval plus 5 3

Defining an addition function for Pos and an instance of Plus Pos allows plus to be used to add both Pos and Nat values:

def Pos.plus : Pos → Pos → Pos
  | Pos.one, k => Pos.succ k
  | Pos.succ n, k => Pos.succ (n.plus k)

instance : Plus Pos where
  plus := Pos.plus

def fourteen : Pos := plus seven seven

Because there is not yet an instance of Plus Float, attempting to add two floating-point numbers with plus fails with a familiar message:

#eval plus 5.2 917.25861

failed to synthesize instance
  Plus Float

These errors mean that Lean was unable to find an instance for a given type class.

Overloaded Addition

Lean's built-in addition operator is syntactic sugar for a type class called HAdd, which flexibly allows the arguments to addition to have different types. HAdd is short for heterogeneous addition. For example, an HAdd instance can be written to allow a Nat to be added to a Float, resulting in a new Float. When a programmer writes x + y, it is interpreted as meaning HAdd.hAdd x y.

While an understanding of the full generality of HAdd relies on features that are discussed in another section in this chapter, there is a simpler type class called Add that does not allow the types of the arguments to be mixed. The Lean libraries are set up so that an instance of Add will be found when searching for an instance of HAdd in which both arguments have the same type.

Defining an instance of Add Pos allows Pos values to use ordinary addition syntax:

instance : Add Pos where
  add := Pos.plus

def fourteen : Pos := seven + seven

Conversion to Strings

Another useful built-in class is called ToString. Instances of ToString provide a standard way of converting values from a given type into strings. For example, a ToString instance is used when a value occurs in an interpolated string, and it determines how the IO.println function used at the beginning of the description of IO will display a value.

For example, one way to convert a Pos into a String is to reveal its inner structure. The function posToString takes a Bool that determines whether to parenthesize uses of Pos.succ, which should be true in the initial call to the function and false in all recursive calls.

def posToString (atTop : Bool) (p : Pos) : String :=
  let paren s := if atTop then s else "(" ++ s ++ ")"
  match p with
  | Pos.one => "Pos.one"
  | Pos.succ n => paren s!"Pos.succ {posToString false n}"

Using this function for a ToString instance:

instance : ToString Pos where
  toString := posToString true

results in informative, yet overwhelming, output:

#eval s!"There are {seven}"

"There are Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))"

On the other hand, every positive number has a corresponding Nat. Converting it to a Nat and then using the ToString Nat instance (that is, the overloading of toString for Nat) is a quick way to generate much shorter output:

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

instance : ToString Pos where
  toString x := toString (x.toNat)

#eval s!"There are {seven}"

"There are 7"

When more than one instance is defined, the most recent takes precedence. Additionally, if a type has a ToString instance, then it can be used to display the result of #eval even if the type in question was not defined with deriving Repr, so #eval seven outputs 7.

Overloaded Multiplication

For multiplication, there is a type class called HMul that allows mixed argument types, just like HAdd. Just as x + y is interpreted as HAdd.hAdd x y, x * y is interpreted as HMul.hMul x y. For the common case of multiplication of two arguments with the same type, a Mul instance suffices.

An instance of Mul allows ordinary multiplication syntax to be used with Pos:

def Pos.mul : Pos → Pos → Pos
  | Pos.one, k => k
  | Pos.succ n, k => n.mul k + k

instance : Mul Pos where
  mul := Pos.mul

With this instance, multiplication works as expected:

#eval [seven * Pos.one,
       seven * seven,
       Pos.succ Pos.one * seven]

[7, 49, 14]

Literal Numbers

It is quite inconvenient to write out a sequence of constructors for positive numbers. One way to work around the problem would be to provide a function to convert a Nat into a Pos. However, this approach has downsides. First off, because Pos cannot represent 0, the resulting function would either convert a Nat to a bigger number, or it would return Option Pos. Neither is particularly convenient for users. Secondly, the need to call the function explicitly would make programs that use positive numbers much less convenient to write than programs that use Nat. Having a trade-off between precise types and convenient APIs means that the precise types become less useful.

In Lean, natural number literals are interpreted using a type class called OfNat:

class OfNat (α : Type) (_ : Nat) where
  ofNat : α

This type class takes two arguments: α is the type for which a natural number is overloaded, and the unnamed Nat argument is the actual literal number that was encountered in the program. The method ofNat is then used as the value of the numeric literal. Because the class contains the Nat argument, it becomes possible to define only instances for those values where the number makes sense.

OfNat demonstrates that the arguments to type classes do not need to be types. Because types in Lean are first-class participants in the language that can be passed as arguments to functions and given definitions with def and abbrev, there is no barrier that prevents non-type arguments in positions where a less-flexible language could not permit them. This flexibility allows overloaded operations to be provided for particular values as well as particular types.

For example, a sum type that represents natural numbers less than four can be defined as follows:

inductive LT4 where
  | zero
  | one
  | two
  | three
deriving Repr

While it would not make sense to allow any literal number to be used for this type, numbers less than four clearly make sense:

instance : OfNat LT4 0 where
  ofNat := LT4.zero

instance : OfNat LT4 1 where
  ofNat := LT4.one

instance : OfNat LT4 2 where
  ofNat := LT4.two

instance : OfNat LT4 3 where
  ofNat := LT4.three

With these instances, the following examples work:

#eval (3 : LT4)

LT4.three

#eval (0 : LT4)

LT4.zero

On the other hand, out-of-bounds literals are still not allowed:

#eval (4 : LT4)

failed to synthesize instance
OfNat LT4 4

For Pos, the OfNat instance should work for any Nat other than Nat.zero. Another way to phrase this is to say that for all natural numbers n, the instance should work for n + 1. Just as names like α automatically become implicit arguments to functions that Lean fills out on its own, instances can take automatic implicit arguments. In this instance, the argument n stands for any Nat, and the instance is defined for a Nat that's one greater:

instance : OfNat Pos (n + 1) where
  ofNat :=
    let rec natPlusOne : Nat → Pos
      | 0 => Pos.one
      | k + 1 => Pos.succ (natPlusOne k)
    natPlusOne n

Because n stands for a Nat that's one less than what the user wrote, the helper function natPlusOne returns a Pos that's one greater than its argument. This makes it possible to use natural number literals for positive numbers, but not for zero:

def eight : Pos := 8

def zero : Pos := 0

failed to synthesize instance
  OfNat Pos 0

Exercises

Another Representation

An alternative way to represent a positive number is as the successor of some Nat. Replace the definition of Pos with a structure whose constructor is named succ that contains a Nat:

structure Pos where
  succ ::
  pred : Nat

Define instances of Add, Mul, ToString, and OfNat that allow this version of Pos to be used conveniently.

Even Numbers

Define a datatype that represents only even numbers. Define instances of Add, Mul, and ToString that allow it to be used conveniently. OfNat requires a feature that is introduced in the next section.

HTTP Requests

An HTTP request begins with an identification of a HTTP method, such as GET or POST, along with a URI and an HTTP version. Define an inductive type that represents an interesting subset of the HTTP methods, and a structure that represents HTTP responses. Responses should have a ToString instance that makes it possible to debug them. Use a type class to associate different IO actions with each HTTP method, and write a test harness as an IO action that calls each method and prints the result.

Functional Programming in Lean