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 



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 



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 



Yet another option is using match expressions
Lean  Scala 



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 {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 



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



The keyword structure defines several things at once:
 A type (
Color
)  A constructor (
Color.mk
)  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 



3. Algebraic Data Types
option
and sum
are good examples of simple ADTs defined in the std library:
option
Lean  Scala 



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 



3.1 Recursive definitions
Let’s see how the ubiquitous list
data structure is defined in Lean:
Lists
Lean  Scala 





(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 



The Scala version carries both type and valuelevel information, as we’re going to use it to prove some propositions.
Addition
The most basic operation with numbers is addition:
Lean (try it)



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





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):






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 variableA
that works for any universe (universe polymorphic). In this situation Leans creates a universe variable, sayu₁
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 useType*
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 typeA
in universeu
, the resulting typeI
can’t live in a universe smaller thanu
(with one exception,Prop
, to be discussed in the future).Long story short, using a single universe variable
u
ensures thatVec
inhabits the same universe that the parameterA
, 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:






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.

Scala 3 Reference manual.