Typista.org

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 = nextnext        := rfl
example: iter next 3 = nextnextnext := 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.

Addition

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:}, Vecn -> Vecn -> Vecn 
  | _ 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

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