Typista.org

Lean for Scala programmers - Part 3

April 16, 2021

In the previous installment we discussed inductive types and patern matching.

Today we’re going to talk about Dependent Types and Type Classes.

If you want to follow along you can use online editors:

Dependent functions

A function ABA \to B between two sets A,BA, B is defined in mathematics as a collection of pairs f:={(a,b)}A×Bf := \{(a, b)\} \subset A \times B with the property that elements aa of AA can appear at most once.

normal-function

A dependently typed function is a generalization of this concept:

dependent-function

Each element f(a)f(a) is allowed to be a member of a different set that depends on aa.

This construction gives rise to a set-level function BB that assigns a set B(a)B(a) to each element aAa \in A.

Observe that if this function BB is constant (i.e. it maps all elements aa to a single set) then we are back to the regular definition of non-dependent functions.

Example: Vector fields

At every point pp of a circle S1S^1, consider a vector V(p)V(p) on the tangent space TpS1T_{p}S^{1} at this point:

vector-field

Since each V(p)V(p) lives in a different tangent space TpS1T_{p}S^{1} (that depends on pp), it makes sense to regard VV as a dependent function.

Example: operations on tuples

A very common example of dependent types in Scala 3 is obtaining components of tuples at specific positions:

val t: (Int, String, Boolean) = (0, "", false)

assert( t.apply(0) == 0 )
assert( t.apply(1) == "" )
assert( t.apply(2) == false )

We can see how apply produces a value of a type that depends on the input index:

tuple-apply

In fact most generic tuple operations use dependent types.

Dependent functions in Lean

In Lean the type of a regular function ff from AA to BB is written as

f: A -> B

here the codomain B is the same for every element a of the domain A.

In a dependent function we need a way to indicate exactly how the codomain depends on each element of the domain.

The signature of a dependent function f from A to B(a) is written in Lean like this:

syntax-lean

which can be represented as a string diagram like so:

syntax-string-diagram

(Π can be entered as \Pi)

Dependent function types are also called Pi types

Detailed example: variable number of arguments

Consider a function adder that takes:

  1. A number nn representing extra arguments
  2. An initial value accacc
  3. nn arguments

It returns the sum of the initial value and extra arguments.

For example

example: adder 0 5        = (5 :) := rfl
example: adder 1 10 11    = (21:) := rfl
example: adder 2 18 17 12 = (47:) := rfl

i.e. the first argument is the number of extra arguments after the 2nd argument.

(This example is described in Edwin Brady’s Type-Driven Development with Idris)

We will proceed in two steps:

  1. Define a type level function that calculates the return type: a function with nn parameters:
open nat

def Adder:-> Type
  | 0        :=| (succ k) :=-> (Adder k)


example: Adder 0 =:= rfl
example: Adder 1 = (->)      := rfl
example: Adder 2 = (->->) := rfl
  1. Define a regular function, whose signature is computed by Adder based on the 1st argument:
--                  acc
--                   | 
def adder: Π (n:),-> (Adder n)
  | 0        acc := acc
  | (succ k) acc := λ n, adder k (n + acc)
--     |  
--     n  


-- adder 0 acc =                  acc
-- adder 1 acc = λ n,         n + acc
-- adder 2 acc = λ n n1, n1 + n + acc

-- with types:

-- adder 0 : ℕ -> ℕ
-- adder 1 : ℕ -> ℕ -> ℕ
-- adder 2 : ℕ -> ℕ -> ℕ -> ℕ

example: (adder 0) 5        = (5 :) := rfl
example: (adder 1) 10 11    = (21:) := rfl
example: (adder 2) 18 17 12 = (47:) := rfl

So adder n produces a function whose type depends on n:

dependent-function

Dependent Functions in Scala 3

Match types

Scala 3 supports a similar form of dependent typing using match types.

We follow the same steps as in Lean:

  1. Define a type level function that calculates the return type:
import compiletime.ops.int.S

type Adder[N <: Int] = N match
  case 0    =>  Int
  case S[k] => (Int => Adder[k & Singleton])


summon[ Adder[0] =:=  Int               ]
summon[ Adder[1] =:= (Int => Int)       ]
summon[ Adder[2] =:= (Int => Int => Int)]
  1. Define a function, whose signature is computed by Adder based on the 1st argument:
inline def adder[N <: Int & Singleton](n: N)(acc: Int): Adder[N] =
  inline n match
    case _: 0    => acc
    case _: S[k] => n => adder(constValue[k & Singleton])(n + acc)


assert( adder(0)(5)          == 5  )
assert( adder(1)(10)(11)     == 21 )
assert( adder(2)(18)(17)(12) == 47 )

Here we can see how the fact that types are not first class in Scala introduces some complexities:

  • Singleton is needed so that adder(0) is inferred as adder[0](0) and not adder[Int](0).
  • After pattern matching on the type _: S[k] we obtain the type k of the predecessor n - 1.
  • In order to continue the process we need to obtain the value associated with the singleton type k. For this we use constValue.
  • But constValue only works for values known at compile time, so we have to use inline match and also inline the whole function.

Path-dependent types + implicit resolution

Another option is to use a type class to bundle the output type and the adder function, and construct both type and function in lockstep:

trait Bundle[N <: Int]:
  type Adder
  def adder: Int => Adder

Now the index is kept purely on the type variable N so adder only needs to handle the accumulated value acc.

Due to a idiosyncrasy of Scala we need to create a helper type function BundleWithAdder to manually propagate type information (this is the Aux pattern common in shapeless).

type BundleWithAdder[N <: Int, A] =
  Bundle[N] { type Adder = A }

// base case: Bundle[0]

given BundleWithAdder[0, Int] =
  new Bundle[0]:
    type Adder = Int
    def adder = identity

// inductive step: Bundle[K] implies Bundle[S[K]]

given [K <: Int](using predecessor: Bundle[K]): 
  BundleWithAdder[S[K], Int => predecessor.Adder] =
  new Bundle[S[K]]:
    type Adder = Int => predecessor.Adder
    def adder = acc => n => predecessor.adder(n + acc)

Sanity check:

val bundle0 = summon[Bundle[0]]
val bundle1 = summon[Bundle[1]]
val bundle2 = summon[Bundle[2]]

summon[ bundle0.Adder =:=  Int                ]
summon[ bundle1.Adder =:= (Int => Int)        ]
summon[ bundle2.Adder =:= (Int => Int => Int) ]

Taking the singleton type n.type of the term n will kickstart the process:

def adder(n: Int)(acc: Int)(using bundle: Bundle[n.type]) =
  bundle.adder(acc)

assert( adder(0)(5)          == 5  )
assert( adder(1)(10)(11)     == 21 )
assert( adder(2)(18)(17)(12) == 47 )

Type Classes in Lean

Lean has support for type classes by using the keywords class / instance.

Let’s implement the adder function using implicit type class resolution this time:

class Bundle (n:) :=
  (Adder: Type)
  (adder:-> Adder)

This declaration defines a few things:

#print Bundle

-- @[class]
-- structure Bundle : ℕ → Type 1
-- fields:
-- Bundle.Adder : Π (n : ℕ) [c : Bundle n], Type
-- Bundle.adder : Π {n : ℕ} [c : Bundle n], ℕ → Bundle.Adder n

So a class is just a structure with an annotation @[class].

Note how every member field acquired two extra parameters:

  • The class argument (n: ℕ)
  • An implicit instance [c : Bundle n] (indicated by the square brackets)

Something a bit surprising is that there is no way to pass a single implicit argument explicitly. This makes using functions defined as type class members awkward in some cases.

One way to overcome this is to transform the function into a variant where every argument is explicit, by prefixing the name with an @:

#check @Bundle.adder

-- Bundle.adder : Π {n : ℕ} [c : Bundle n], ℕ → Bundle.Adder n

with this in mind let’s define the adder function:

def adder (n acc:) [c: Bundle n]: Bundle.Adder n :=
  @Bundle.adder n c acc

The only thing we did was to rearrange the parameters of Bundler.adder: both n and acc are now explicit, and the implicit Bundle n was moved to the end of the list.

(This makes adder much easier to call than Bundle.adder as can be seen below)

We need two Bundle instances again, corresponding to the base case and the inductive step:

instance bundleBase: Bundle 0 := {
  Adder :=,
  adder := id
}

instance bundleStep (k:) [predecessor: Bundle k] : Bundle (succ k) := {
  Adder :=-> predecessor.Adder,
  adder := λ acc n, adder k (n + acc)
}

Notes:

  • id is the identity function
  • adder k (n + acc) is using the implicit instance in scope (predecessor), so we don’t need to pass it manually.

Sanity check:

example: (adder 0) 5        = (5 :) := rfl
example: (adder 1) 10 11    = (21:) := rfl
example: (adder 2) 18 17 12 = (47:) := rfl

In summary, we need to handle 4 cases:

n Type (Adder) Term (adder)
0 identity function
k + 1 ℕ -> predecessor.Adder λ acc n, adder k (n + acc)

(The two rows come from the fact that natural numbers are an inductive type with two cases: zero and succ)

There’s a certain symmetry between the two approaches we’ve described:

  • Regular dependent functions allows us to define the Type column at once and the Term column at once.
  • Chained type classes allows us to define the n = 0 row at once and the n = k + 1 row at once.

Propositions

Note: Lean defines two synonyms for Π: forall and . By convention the forall versions are used when the dependent function produces propositions.

Properties of natural numbers

Consider the statement:

For all natural numbers, n+0=nn + 0 = n

The expression n+0=nn + 0 = n is a proposition that depends on nn, and so the statement can be modeled as a dependent function ff from natural numbers to a family of propositions:

lemma f (n :) : n + 0 = n :=
	rfl
propositions

Algebraic structures

Here’s how one could define a monoid in Lean

class Monoid (M: Type*) :=
  (mul : M -> M -> M)
  (one : M)
  (mul_assoc :(a b c : M), mul (mul a b) c = mul a (mul b c))
  (one_mul   :(a : M), mul one a = a)
  (mul_one   :(a : M), mul a one = a)

In this kind of situations we rely heavily on dependent types to encode all the laws associated with the structure at hand. In this example each law is a dependent function from M to propositions.

Here’s a monoid instance for addition of natural numbers:

instance monoidNat: Monoid:= {
  mul := (+),
  one := 0,
  mul_assoc := nat.add_assoc,
  one_mul   := nat.zero_add,
  mul_one   := nat.add_zero,
}

Luckily in this case the basic properties have already been proved in the std library, so we can just delegate to them.

A note on syntax

The reason for the name “Pi types” (and the symbol Π) is the following :

In math, it is common to use the notation BAB^A to indicate the set of all functions from AA to BB.

For simplicity let’s assume that AA is finite (and has cardinality A=n|A| = n)

Then we can define:

BA:=Πa:A B=B×B××BA timesB^A := \Pi_{a: A}\ B = \underbrace{B \times B \times \cdots \times B}_{|A|\ \mathrm{ times}}

and each element fΠa:A Bf \in \Pi_{a: A}\ B has the form (fa1,fa2,,fan)(f_{a_1}, f_{a_2}, \dots, f_{a_n}).

In other words, for each aiAa_i \in A we can find an element faiBf_{a_i}\in B at the position ii.

Given such a tuple we can create a function f:ABf: A \to B by the rule

f(ai):=faif(a_i) := f_{a_i}

conversely, given a function f:ABf: A \to B we can create the tuple (f(a1),f(a2),)Πa:A B(f(a_1), f(a_2), \dots) \in \Pi_{a: A}\ B

In a dependent function we let BB depend on aAa \in A like so:

Πa:A Ba=Ba1×Ba2××Ban\Pi_{a: A}\ B_a = B_{a_1} \times B_{a_2} \times \cdots \times B_{a_n}

This is the motivation for the syntax:

Π (a: A), B a

When B does not depend on a: A this becomes

Π (_: A), B

and we can use the syntactic sugar

A -> B

Dependent products

There is another important example of dependent types called Sigma types or dependent product.

Consider the regular cartesian product of two sets AA, BB:

normal-product

This represents all possible combinations of elements from both sets:

(a,x),(a,y),(a,w),(b,x),(b,y),(b,w)(a, x), (a, y), (a, w), (b, x), (b, y), (b, w)

The dependent product type Σ(x:A),B(x)\Sigma (x: A), B(x) denotes the type of pairs (a,b)(a, b) where aAa \in A and bB(a)b \in B(a)

dependent-product

The diagram depicts a situation where xx and yy are elements of B(a)B(a) and wB(b)w \in B(b). In this case the inhabitants of the dependent product Σ(x:A),B(x)\Sigma (x: A), B(x) are the pairs:

(a,x),(a,y),(b,w)(a, x), (a, y), (b, w)

Dependent products in Lean

In Lean dependent products are defined as the inductive type:

universes u v

structure sigma {A: Type u} (B: A -> Type v) :=
  (fst: A) (snd: B fst)

The symbol Σ can be used as well (typed as \Si):

Σ (x : A), B x

Dependent products can be constructed like so:

sigma.mk a b

Dependent products in Scala

Dependent products can be encoded directly with path-dependent types.

path-dependent-types
trait Fn0:
  type B

class Sigma[A <: Fn0](fst: A, snd: fst.B)

In general, every function that uses path-dependent types in its parameters list is an example of Sigma types in action:

def f(a: A, b: a.B) = ...

Next time we’ll talk about proofs and tactics. Stayed tunned!

Resources