Lean and Type Classes

Stepping away from our recent logic-focused topics, we will return to working with our custom natural number type, MyNat, following the approach in "Introduction to Lean for Beginners: Hands-on Formal Mathematics Library Development". In this post, we will explore how to implement type class instances to allow MyNat to support numeric literals and arithmetic operators.

A Quick Recap of MyNat

First, let's look back at how we defined MyNat.

-- Peano axioms
inductive MyNat where
  | zero
  | succ (n : MyNat)

-- Add
def MyNat.add (m n : MyNat) : MyNat :=
  match n with
  | .zero => m
  | .succ n => succ (add m n)

MyNat is built from just two constructors: zero (representing 0) and succ (the successor of a given natural number). MyNat.add is defined by recursion on the structure of n. Conceptually, it peels off each succ from n one by one and wraps m with a corresponding succ.

Interpreting Numeric Literals as MyNat

As it stands, writing out MyNat values is quite cumbersome, requiring expressions like MyNat.zero or MyNat.succ MyNat.zero every single time. To fix this, we will write a conversion function from Lean's built-in natural number type, Nat, to MyNat.

def MyNat.ofNat (n : Nat) : MyNat :=
  match n with
  | 0 => MyNat.zero
  | n + 1 => MyNat.succ (MyNat.ofNat n)

The logic is straightforward: it matches the Nat value as either 0 or n + 1, and maps them to MyNat.zero and MyNat.succ, respectively.

Using this conversion function, we can enable Lean to interpret numeric literals directly as MyNat values. In Lean, how numeric literals like 0 or 1 are interpreted is determined by a type class named OfNat. By implementing an OfNat instance for MyNat, we can resolve numeric literals into MyNat values.

-- The numeric literal is interpreted as type MyNat.
@[default_instance]
instance (n : Nat) : OfNat MyNat n where
  ofNat := MyNat.ofNat n

If we check this using #check, we can verify that numeric literals are now successfully interpreted as MyNat.

#check 0 -- 0 : MyNat
#check 1 -- 1 : MyNat

Enabling Addition with the + Operator

Next, we will register our previously defined MyNat.add so that it can be used with the + operator. Much like OfNat, this is achieved by implementing an instance for the Add type class.

instance : Add MyNat where
  add := MyNat.add

def MyNat.one := MyNat.succ MyNat.zero

#eval MyNat.zero + 0 -- MyNat.zero
#eval MyNat.one + 1 -- MyNat.succ (MyNat.succ (MyNat.zero))

We can see that the + operator works seamlessly between explicitly constructed values like MyNat.zero or MyNat.one and numeric literals. However, at this point, #eval still outputs the raw structural representation, such as MyNat.succ (MyNat.succ (MyNat.zero)), which makes it a bit hard to read.

Formatting for Better Readability

Finally, we will configure #eval to display the evaluated results as familiar numbers. In Lean, you can customize how a type is displayed by implementing an instance of the Repr type class.

To do this, we first create a function to convert MyNat back into Nat.

def MyNat.toNat (n : MyNat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => MyNat.toNat n + 1

Notice that we can use 0 and n + 1 in the match patterns here thanks to the OfNat instance we implemented for MyNat earlier. Now, we use this toNat function to implement the Repr instance.

instance : Repr MyNat where
  reprPrec n _ := repr n.toNat

The reprPrec function converts a value into a displayable string format (specifically, a Format object). Our implementation converts the MyNat value into a Nat using toNat, and then simply borrows the standard display format of that Nat. With this added, #eval results are now cleanly printed as standard numbers.

#eval 0 + 0 -- 0
#eval 1 + 1 -- 2