# Lean for Scala programmers - Part 2

March 14, 2021

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

• Type universes
• 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.

# 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.

Lean Scala
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 a type and a namespace in both Lean and Scala.

Elements can be accessed like so

Weekday.sunday

alternatively the namespace can be opened:

Lean Scala
open Weekday 
import Weekday.*

### 1.1 Pattern matching

There are several ways to pattern match on inductive types. One of the most primitives is the function cases_on:

def number_of_day (d: Weekday): ℕ :=
Weekday.cases_on d 1 2 3 4 5 6 7

example: number_of_day sunday = 1 := rfl

This function is generated automatically for all inductive types (and there’s no direct equivalent in Scala for this).

A more common approach is to use pattern matching:

Lean Scala
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

Yet another option is using match expressions

Lean Scala
def next (d: Weekday): Weekday :=
match d with
| sunday    := monday
| monday    := tuesday
| tuesday   := wednesday
| wednesday := thursday
| thursday  := friday
| friday    := saturday
| saturday  := sunday
end
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:

try it

def iter {A: Type*} (f: A -> A): ℕ -> (A -> A)
| 0       := id
| (n + 1) := f ∘ (iter 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 λ 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 :=
begin
intro w,
cases w,
repeat { refl },
end

### 1.2 Examples

Some important enumerations are defined in the std library:

Lean Scala
-- a type without inhabitants
inductive empty: Type

-- only one inhabitant
inductive unit: Type
star: unit

inductive bool: Type
| ff: bool
| tt: bool
// built-in: Nothing
sealed trait empty

// built-in: Unit
enum unit:
case star

// built-in: Boolean
enum bool:
case ff, tt

## 2. Structures

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

Lean Scala
structure Color :=
(red  : ℕ)
(green: ℕ)
(blue : ℕ)
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 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:

Lean Scala
structure prod (A B: Type*) :=
(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

option and sum are good examples of simple ADTs defined in the std library:

#### option

Lean Scala
inductive option (A: Type*)
| none: option
| some (a: A): option
enum Option[+A]:
case None
case Some(a: A)

Notice how we’re adding an explicit type ascription : option on each case. This is required in general except for simple types like enumerations and structures.

Also, even though we’re writing just : option, Lean transforms this internally into : option A.

#### sum

Lean Scala
inductive sum (A B: Type*)
| inl (a: A): sum
| inr (b: B): sum
enum Sum[A, B]:
case Inl(a: A)
case Inr(b: B)

### 3.1 Recursive definitions

Let’s see how the ubiquitous list data structure is defined in Lean:

#### Lists

Lean Scala
inductive list (T: Type*)
| nil: list
| cons (hd: T) (tl: list): list
enum List[+T]:
case Nil
case Cons(hd: T, tl: List[T])
notation h :: t  := list.cons h t

def lst := 1 :: 2 :: list.nil
extension [T] (h: T)
def :: (t: List[T]) = List.Cons(h,t)

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

(the Scala version is not the one from the std library)

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

#### 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).

Lean Scala
inductive nat
| zero: nat
| succ (n: nat): nat
enum Nat:
case Zero()
case Succ[N <: Nat](n: N)

The Scala version carries both type and value-level information, as we’re going to use it to prove some propositions.

The most basic operation with numbers is addition:

Lean (try it)

 open nat -- this defines two rules: -- 1) add l zero = l -- 2) add l (succ r) = succ (add l r) def add (l: nat): nat -> nat | zero := l | (succ r) := succ (add r) example: add 1 2 = 3 := rfl -- by definition of add: lemma add_zero (l: nat): add l 0 = l := rfl lemma add_succ (l r: nat): add l (succ r) = succ (add l r) := rfl

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

Scala 3:

 import Nat.* // This defines two rewrite rules: // 1) Add[L, Zero] => L // 2) Add[L, Succ[r]] => Succ[Add[L, r]] type Add[L <: Nat, R <: Nat] <: Nat = R match case Zero => L case Succ[r] => Succ[Add[L, r]] // The value-level counterpart. // This is a dependent function: the return type Add[L, R] // depends on the provided value (l: L) def add[L <: Nat, R <: Nat](l: L, r: R): Add[L, R] = r match case _: Zero => l case Succ(t): Succ[_] => Succ(add(l, t)) type _0 = Zero type _1 = Succ[_0] type _2 = Succ[_1] type _3 = Succ[_2] // sanity check: summon[ Add[_1, _2] =:= _3 ] val _0: _0 = Zero() val _1: _1 = Succ(_0) val _2: _2 = Succ(_1) val _3: _3 = Succ(_2) // Dependent types allow us to create very precise types: // without dependent types: add(_1, _2): Nat // with dependent types: add(_1, _2): _3 // We can even prove a few things: def add_zero[L <: Nat]: Add[L, _0] =:= L = <:<.refl def add_succ[L <: Nat, R <: Nat]: Add[L, Succ[R]] =:= Succ[Add[L, R]] = <:<.refl

## 4. Generalized Algebraic Data Types

GADTs are called inductive families in Lean.

#### A simple language

Here’s how the ubiquitous arithmetic evaluator Expr looks in Lean:

inductive Expr : Type -> Type
| I (n: ℕ) : Expr ℕ
| B (b: bool) : Expr bool
| Add (e1: Expr ℕ) (e2: Expr ℕ) : Expr ℕ
| Mul (e1: Expr ℕ) (e2: Expr ℕ) : Expr ℕ

Scala 3:

enum Expr[A]:
case I(n: Int) extends Expr[Int]
case B(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]

Observe that Expr is a function Type -> Type.

Here’s an interpreter for this language:

def eval: Π {A: Type}, Expr A -> A
| _ (I n) := n
| _ (B b) := b
| _ (Add e1 e2) := eval e1 + eval e2
| _ (Mul e1 e2) := eval e1 * eval e2

Each case in the body of eval takes two arguments: a type A and an Expr A . But instead of

| A (I n) := n

(for example) we can write:

| _ (I n) := n

Since (I n) has type Expr ℕ , we can ask Lean to infer A = ℕ by using the underscore syntax _.

The Π in the signature of eval indicates that this is a dependently typed function. This will be explored at length on the next installment.

In Scala:

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

#### Vectors

Another common example are sized vectors.

Lean (try it):

 universe u inductive Vec (A: Type u): ℕ → Type u | vnil : Vec 0 | cons {n: ℕ} (a: A) (v: Vec n) : Vec (n + 1) open Vec  local notation h :: t := cons h t def head {A: Type*} {n: ℕ}: Vec A (n + 1) -> A | (h :: t) := h def add: Π {n: ℕ}, Vec ℕ n -> Vec ℕ n -> Vec ℕ n | _ vnil vnil := 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.

Interlude: Universe variables

So far we’ve used A: Type* to declare a type variable A that works for any universe (universe polymorphic). In this situation Leans creates a universe variable, say u₁ and uses it instead.

We can introduce universe variables explicitly with statements like

universe u
-- or
universes u v

In the definition of Vec , if we were to use Type* in both places Lean would try to crate two independent universe variables (say, u₁, u₂).

This would be incorrect, as there are some constraints that universes variables most follow: If we create an inductive type I parameterized by a type A in universe u, the resulting type I can’t live in a universe smaller than u (with one exception, Prop, to be discussed in the future).

Long story short, using a single universe variable u ensures that Vec inhabits the same universe that the parameter A, satisfying Lean’s universe rules.

def v := 1 :: 1 :: vnil

example: head v = 1 := rfl
example: add v v = 2 :: 2 :: vnil := rfl

-- doesn't compile!
-- head 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

// head(VNil) 