The previous installment we gave an initial look at some basic Lean features:

• Propositions
• Proofs
• Tactics

Today we’re going to focus on two topics:

• creating data structures via inductive types
• using pattern matching to transform or consume inductive types.

Latest revision: Sep 4, 2022

Inductive types

Inductive types are the type theory version of what in functional programming is known as Algebraic Data Types.

1. Enumerations

The simplest kind: not parameterized, nor recursive.

inductive Weekday
  | sunday
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday  

enum Weekday:
  case Sunday 
  case Monday 
  case Tuesday 
  case Wednesday 
  case Thursday 
  case Friday 
  case Saturday 

This definition creates 1) a type 2) a namespace 3) exactly 7 ways to construct values of type Weekday.

Elements can be accessed like so

Weekday.sunday

alternatively the namespace can be opened:

open Weekday 

import Weekday.*

An important difference is that in Scala each constructor has its own type, whereas in Lean constructors are just functions (without arguments in this case).

This has a consequence: if we want to define operations that only work on some constructors we need to come up with a way to distinguish them in the type system, perhaps using another type as index .

1.1 Pattern matching

There are several ways to pattern match on inductive types.

A common approach is to use a function defined by cases:

 def next: Weekday -> Weekday
  | sunday    => monday 
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

val next: Weekday => Weekday =
  case Sunday    => Monday
  case Monday    => Tuesday
  case Tuesday   => Wednesday
  case Wednesday => Thursday
  case Thursday  => Friday
  case Friday    => Saturday
  case Saturday  => Sunday

which is syntactic sugar for match expressions:

def next' (d: Weekday) : Weekday := 
  match d with
  | sunday    => monday 
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

def next(d: Weekday): Weekday = 
  d match
    case Sunday    => Monday
    case Monday    => Tuesday
    case Tuesday   => Wednesday
    case Wednesday => Thursday
    case Thursday  => Friday
    case Friday    => Saturday
    case Saturday  => Sunday

Let’s prove that applying next 7 times is the identity function.

First we need a way to iterate a function a number of times:

def iter (f: A -> A): Nat -> (A -> A) 
  | 0     => id
  | n + 1 => f ∘ (iter f n)


example: iter next 0 = id                 := rfl
example: iter next 1 = next               := rfl
example: iter next 2 = next ∘ next        := rfl
example: iter next 3 = next ∘ next ∘ next := rfl

id is the identity function fun x => x. The composition operator ∘ can be entered as \circ.

Observe how we’re using n + 1 as a pattern, allowing us to extract n and pass it to the next iter call. This is similar to deconstructing a list as h :: t.

In both cases Lean can verify that the recursive invocation is given a smaller data structure, and that the recursion will eventually terminate.

Now we can state and prove the proposition:

for all weekdays, the function next has period 7

example: ∀ (w: Weekday), (iter next 7) w = w := by
  intro w
  cases w
  repeat { rfl }

1.2 Examples

Some important enumerations are defined in the std library:

-- a type without inhabitants

inductive Empty: Type

-- a proposition without inhabitants; that means that it's imposible to prove.
-- This is taken as the definition of False.

inductive False : Prop

-- a proposition with only one way to prove it: True.intro

inductive True : Prop where
  | intro : True
  

2. Structures

Structures in Lean are inductive definitions with only one case, and one or more fields.

structure Color where
  red  : Nat
  green: Nat
  blue : Nat
  

case class Color(
  red  : Int,
  green: Int,
  blue : Int
)

The keyword structure defines several things at once:

1. A type (Color)
2. A constructor (Color.mk)
3. A getter function Color -> Nat for each field (Color.red, Color.green, Color.blue)

Lean provides a limited form of dot notation:

def yellow := Color.mk 255 255 0

example: yellow.red   = 255 := rfl
example: yellow.green = 255 := rfl
example: yellow.blue  = 0   := rfl

Structures can have parameters; for example here’s how the product of two types A and B is defined in the std library:

structure Prod (A B) where
  fst: A 
  snd: B
  
def t := Prod.mk 1 "one"

case class Prod[A, B](
  fst: A, 
  snd: B
)
val t = Prod(1, "one")

3. Algebraic Data Types

Here’s a simplified version of Option and Sum as defined in the std library. They are good examples of simple ADTs.

inductive Option (A)
  | none
  | some (a: A)
  
inductive Sum (A B)
  | inl (a: A)
  | inr (b: B)  

enum Option[+A]:
  case None
  case Some(a: A)

enum Sum[A, B]:
  case Inl(a: A)
  case Inr(b: B)

3.1 Recursive definitions

List is different from Option and Product in that a list can contain other lists of the same type.

3.1.1 Lists

inductive List (T)
  | nil
  | cons (head: T) (tail: List T)
    
infixr:67 " :: " => List.cons
notation "[" "]" => List
.nil

def lst := 1 :: 2 :: []  

enum List[+T]:
  case Nil
  case Cons(head: T, tail: List[T])

extension [T] (h: T) 
  def :: (t: List[T]) = List.Cons(h,t)


val lst = 1 :: 2 :: List.Nil

notation is not really an extension method, but rather something closer to a macro.

3.1.2 Natural numbers

The natural numbers (Nat) are defined inductively in Lean.

(number literals are provided via type classes, which we’ll explore in the future).

inductive Nat
  | zero
  | succ (n: nat)

Unfortunately Nat is not available in Scala’s std library but we could create one like so:

enum Nat:
  case Zero()
  case Succ[N <: Nat](n: N)

(This version carries both type and value-level information).

3.1.3 Addition

Addition of two natural numbers as just created can be defined via two transformation rules:

1. add l zero => l
2. add l (succ r) => succ (add l r)

Lean 4

def add (l: Nat): Nat -> Nat
  | zero   => l
  | succ r => succ (add l r)

Numbers are normally represented using literals like 0, 1, etc, so we can write:

def add (l: Nat): Nat -> Nat
  | 0     => l
  | r + 1 => (add l r) + 1

example: add 1 2 = 3 := rfl

-- by definition of add:

theorem add_zero (l: Nat) : add l 0 = l := by rfl

theorem add_succ (l r: Nat): add l (r + 1) = (add l r) + 1:= by rfl  

Proving add 0 + m = m on the other hand requires a proof by induction, which we’ll discuss in the future.

4. Generalized Algebraic Data Types

GADTs are called inductive families in Lean.

Here are two examples:

4.1 A simple language

A tiny typed language of arithmetic expressions, that delegates its typing to the host language.

Lean 4

inductive Expr : Type -> Type
  | num (n: Nat)          : Expr Nat
  | bool (b: Bool)        : Expr Bool
  | add (e1 e2: Expr Nat) : Expr Nat
  | mul (e1 e2: Expr Nat) : Expr Nat

Scala 3

enum Expr[A]:
  case Num(n: Int) extends Expr[Int]
  case Bool(b: Boolean) extends Expr[Boolean]
  case Add(e1: Expr[Int], e2: Expr[Int]) extends Expr[Int]
  case Mul(e1: Expr[Int], e2: Expr[Int]) extends Expr[Int]

Here’s an interpreter for this language:

def Expr.eval: Expr A -> A
  | num n => n
  | bool b => b
  | add e1 e2 => e1.eval + e2.eval
  | mul e1 e2 => e1.eval * e2.eval

Scala 3

import Expr.*

def eval[A]: Expr[A] => A =
  case Num(n) => n
  case Bool(b) => b
  case Add(e1, e2) => eval(e1) + eval(e2)
  case Mul(e1, e2) => eval(e1) * eval(e2)

4.2 Vectors

Each Vec is parameterized by a type A and a natural number (a value).

Lean 4

inductive Vec (A: Type) : Nat -> Type
  | vnil : Vec A 0
  | cons {n: Nat} (a: A) (v: Vec A n) : Vec A (n + 1)

infixr:67 " :: " => Vec.cons
notation "[" "]" => Vec.nil

def Vec.head: Vec A (n + 1) -> A
  | h :: _ => h

def Vec.add: Vec Nat n -> Vec Nat n -> Vec Nat n 
  | [],      []        => vnil
  | h1 :: t1, h2 :: t2 => (h1 + h2) :: (add t1 t2)

head takes a vector of length n + 1. Lean can infer that there’s no need to handle the vnil case.

def v: Vec Nat 2 := 1 :: 1 :: []

example: Vec.head v = 1 := rfl
example: Vec.add v v = (2 :: 2 :: [] : Vec Nat _) := rfl

-- doesn't compile!
#check_failure Vec.head Vec.vnil

Scala 3

import compiletime.ops.int._
import compiletime.S

enum Vec[+A, n <: Int]:
  case VNil extends Vec[Nothing, 0]
  case Cons(a: A, v: Vec[A, n]) extends Vec[A, n + 1] 

import Vec.*

extension [A, n <: Int] (a: A) 
  def :: (v: Vec[A, n]): Vec[A, n + 1] = Cons(a, v)

def head[A, n <: Int]: Vec[A, S[n]] => A =
  case VNil                   => ??? // impossible
  case Cons(a, _): Cons[A, _] => a

def add[n <: Int]: (Vec[Int, n], Vec[Int, n]) => Vec[Int, n] =
  case (VNil, VNil)                 => VNil
  case (Cons(h1, t1), Cons(h2, t2)) => (h1 + h2) :: add(t1, t2)

Scala will correctly reject head(VNil), but will still complain if we don’t add the useless case VNil => ???.

val v = 1 :: 1 :: VNil

assert( head(v) == 1 )
assert( add(v, v) == 2 :: 2 :: VNil )

// Doesn't even compile:
// head(VNil)

In the next episode of this series we’ll discuss dependent types at length, getting us closer to our goal of being able to prove some properties of our code.

Resources

• Theorem Proving in Lean.
  Chapter 7: “Inductive types”

• Advanced Functional Programming, by Dr Anil Madhavapeddy, Dr Jeremy Yallop.

  Chapter 9: “Programming with GADTs”

• Scala 3 Reference manual.

  ADTs

  Match types and Dependent Typing