Lean for Scala programmers - Part 1

Over the next few blog posts I'm going to use Lean and Scala to explore the following topics:

• What is a proof assistant, and how is it different from a regular programming language?

• What are dependent types?

• What is a formal proof?

• How does the Curry-Howard isomorphism work in practice?

First impressions of Lean

From Wikipedia:

Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types.

The Lean project was created around 2013 by Leonardo de Moura (at Microsoft Research). Today its development is supported by the nonprofit Lean FRO.

In my opinion, the "killer app" for Lean at the moment is mathlib. It is perhaps the largest single repository of formalized mathematics out there.

This fantastic article in Quanta Magazine does a great job describing some of the momentum around Lean and mathlib.

We'll use Lean 4. If you want to follow along, you can find installation instructions here.

Coincidentally, Scala 3 made some forms of dependently typed programming much simpler. It added match types, type lambdas, dependent function types, and type-level arithmetic (scala.compiletime.ops). Together with the literal types of Scala 2.13, these features let us compute with types. It is my opinion that observing dependently typed constructions in a "native" environment such as Lean can help to understand and demystify some features of Scala's type system.

Audience: Scala intermediate/advanced.
Scala version used: 3.9.0
Lean 4 version: 4.31.0
Latest revision: Sep 23, 2026

Let's start by dissecting a simple example.

1. Calculating the length of a list

Lean 4

def length (ls: List A): Nat :=
  match ls with
    | []     =>  0
    | _ :: t =>  1 + length t

#eval length ["a", "b"]
-- 2

#eval length [Bool, Nat -> Nat, String × String, List Nat]
-- 4

Scala 3

def length[A](ls: List[A]): Int =
  ls match
    case Nil    => 0
    case _ :: t => 1 + length(t)

// example
length(List("a", "b")) == 2

We'll use Tuple types in place of type-level lists:

Scala 3 (type level version)

import compiletime.ops.int._

type Length[T <: Tuple] <: Int = T match
  case EmptyTuple => 0
  case _ *: t     => 1 + Length[t]

// examples
summon[ Length[("a", "b")] =:= 2 ]

summon[ Length[(Boolean, Int => Int, (String, String), List[Int])] =:= 4 ]

A few things need discussion:

Lean commands

We'll be using Lean mostly in interactive mode. For that purpose we'll be using two commands:

Implicit type arguments

Notice that the Lean version never declares A. When Lean finds an unknown name like A in a signature, it adds it automatically as an implicit argument. We can see this with #check:

#check @length
-- @length : {A : Type u_1} → List A → Nat

The curly braces mean that A is implicit: we never pass it ourselves, and Lean infers it from the list at each call site. Scala's [A] plays the same role. (We'll come back to u_1 in a moment.)

This feature is called auto-bound implicits. It's handy for short examples, but many projects (mathlib among them) turn it off with set_option autoImplicit false. In that case you declare A yourself: def length {A : Type u} (ls : List A) : Nat, after a universe u line.

One language for values and types

This example shows one of the biggest differences between dependently typed languages such as Lean and "normal" programming languages like Scala.

Look at the second #eval: the same length function counts a list of strings and a list of types. In Lean, types are ordinary values: Bool is a value of type Type, so [Bool, Nat -> Nat] is just a list of type List Type.

That's also why #check showed Type u_1 instead of Type. Type itself is a value of type Type 1, so to accept a list of types, length must work at every universe level u_1. For ["a", "b"], u_1 is 0; for the list of types, it is 1.

More generally, Lean has a single language for programs and types. The type checker can evaluate ordinary functions while it checks types (we'll use this in the next section), and the compiler can turn the same functions into executable code (via C).

Scala in contrast has basically two languages combined into one: the (pure, functional) type-level language that is "evaluated" at compile time, and the regular Scala term-level code that is compiled into JVM bytecode. That's why we needed two definitions above: length for values and Length for types.

Unicode symbols

Unicode symbols are used a lot in Lean, and many operators have a Unicode notation. For example, A × B is notation for Prod A B (the product of two types). In VS Code you type × as \x.

2. Propositions

The expression

length ["a", "b"] = 2

is a proposition (of type Prop).

Propositions are types (of a special kind) on their own, so they can be used in type position. A value of a proposition is a proof of it:

def myExample: length ["a", "b"] = 2 := sorry

sorry plays the role of Scala's ???: it fits in any type. There is one difference: Lean warns about every declaration that uses sorry, while Scala's ??? compiles without a warning and throws a NotImplementedError at runtime.

When we only want to check a proof, and don't need a name for it, we can use example:

example: length ["a", "b"] = 2 := sorry

There are many ways to create propositions; a common one is using the equality operator (=).

Ok, so how do we create a value of this type?

Equality

example: length ["a", "b"] = 2 := rfl

rfl (short for reflexivity) is a proof of a = a, for any value a. Lean accepts it here because both sides are equal by definition: the type checker evaluates length ["a", "b"] and obtains the equivalent proposition

2 = 2

Scala programmers have seen this idea before. In section 1 we wrote

summon[ Length[("a", "b")] =:= 2 ]

A value of type A =:= B is evidence that the types A and B are equal, and summon asks the compiler to find one. The compiler reduces Length[("a", "b")] to 2 and then uses <:<.refl, which is Scala's version of rfl. In both languages, a proof of an equality is a value that the compiler checks.

On the other hand, rfl can't prove 2 = 3, because the two sides are different values. But "we have no proof" is not the same as "false": some propositions can be neither proved nor disproved. In Lean, a proposition p is false when we can prove its negation ¬p, which is a function p → False. For 2 = 3 that's easy:

example: 2 ≠ 3 := by decide

(2 ≠ 3 is notation for ¬(2 = 3), and the decide tactic proves it by computation.)

This is the basis of the Curry-Howard isomorphism, which represents propositions as types and proofs as programs.

3. Map function on lists

As a second example let's implement map. This time, instead of an explicit match, we define the function by cases (this is just syntactic sugar for fun x => match x with ...):

Lean 4

def map (f: A -> B): List A -> List B
  | []      =>  []
  | a :: as =>  f a :: map f as

example: map (fun x => x + 1) [1, 2, 3] = [2, 3, 4] := rfl

example: map Option [Nat, String] = [Option Nat, Option String] := rfl

Scala 3

def map[A, B](f: A => B): List[A] => List[B] =
  case Nil     => Nil
  case a :: as => f(a) :: map(f)(as)

map((x: Int) => x + 1)(List(1, 2, 3))
// List(2, 3, 4)

Scala 3 (type level version)

import compiletime.ops.int._

type Map[F[_ <: Tuple.Union[As]], As <: Tuple] <: Tuple = As match
  case EmptyTuple => EmptyTuple
  case a *: as    => F[a] *: Map[F, as]

// examples
summon[ Map[[x <: Int] =>> x + 1, (1, 2, 3)] =:= (2, 3, 4) ]

summon[ Map[Option, (Int, String)] =:= (Option[Int], Option[String]) ]

The bound on F needs a word. With a plain F[_], Scala requires a type function that accepts any type, but [x <: Int] =>> x + 1 only accepts integers. The bound Tuple.Union[As] says that F only has to accept the element types of As. The standard library's Tuple.Map uses the same trick.

Note that Scala has a special syntax for type level anonymous functions:

// value level function
(x: Int) => x + 1

// type level function
[X <: Int] =>> X + 1

whereas in Lean the same syntax works for both cases:

#check fun (x: Int) => x + 1
-- fun x => x + 1 : Int → Int

#check fun (T: Type) => Option T
-- fun T => Option T : Type → Type

4. A simple proof

Before wrapping up, let's show off the kind of results that can be proved with Lean.

Lemma: Given an arbitrary function $f: A \to B$, for every list $\mathtt{lst}: \mathtt{List\ A}$ it is true that

$$\mathtt{length}\ (\mathtt{map}\ f \ \mathtt{lst})= \mathtt{length}\ \mathtt{lst}$$

i.e. map does not change the length of a list

def map_length (f: A -> B): (lst: List A) -> length (map f lst) = length lst
  | []     => rfl
  | _ :: t => by simp [length, map, map_length f t]

Let's comment briefly on some key points:

• Given a function f and a list lst, this function creates a proof of the proposition length (map f lst) = length lst.
• Look at the type of map_length: the result type mentions lst, the value of the argument. This is a dependent function type: the type of the result depends on the value that we pass in. This is our first real dependent type!
• Read as logic, the type says: "for every list lst of type List A, mapping f over lst doesn't change its length". A dependent function type is a "for all" statement.
• Since lists are either empty ([]) or of the form h :: t, we define the function by cases:
  • For the empty list, both sides evaluate to 0, so rfl is enough.
  • For h :: t, the recursive call map_length f t gives us a proof of the same statement for the shorter list t. That is the induction hypothesis: a structurally recursive function that returns proofs is a proof by induction.
  • We pass the induction hypothesis to the tactic simp, together with the definitions of length and map. simp unfolds the definitions, rewrites with the hypothesis, and closes the goal.
• Tactics are programs that run at compile time and build the proof term for us. They automate a lot of the boilerplate of writing proofs by hand.

Scala can't follow us here. With match types we can check the lemma for any particular tuple, but the compiler can't prove it for an abstract one:

// does not compile
def mapLength[F[_ <: Tuple.Union[As]], As <: Tuple]: Length[Map[F, As]] =:= Length[As] =
  summon

Match types can't reduce while As is unknown, so there is nothing for the compiler to compute.

It is customary to use the keyword theorem when proving things, and to write the type with ∀ (for all):

theorem map_length' (f: A -> B): ∀ (lst: List A), length (map f lst) = length lst
  | []     => rfl
  | _ :: t => by simp [length, map, map_length' f t]

∀ (lst: List A), ... is just notation for the dependent function type (lst: List A) -> ..., so map_length' has exactly the same type as map_length. (We added a ' to the name because Lean doesn't allow two declarations with the same name.)

Lean's standard library already has this lemma, for the built-in List.length and List.map:

#check @List.length_map
-- @List.length_map : ∀ {α : Type u_1} {β : Type u_2} {as : List α} (f : α → β), (List.map f as).length = as.length

Continue in part 2 with Inductive types, Structures and Algebraic Data Types.

Resources

• Natural Number Game

• Functional Programming in Lean

• Theorem Proving in Lean 4

• Getting started

• Learning Lean