Programming in Dependent Type Theory

All code in this ar­ti­cle was writ­ten in the Lean the­o­rem prover, which means you can copy any of it and paste it here to try it out.

Arith­metic and Interaction

While Lean is nom­i­nally an in­ter­ac­tive the­o­rem prover, much of the power of type the­ory comes from the fact that you can treat it like a pro­gram­ming lan­guage.

There are a few differ­ent com­mands for in­ter­act­ing with Lean. The one I make the most use of is the check com­mand, which prints out the type of the ex­pres­sion fol­low­ing it. So, for ex­am­ple, check 3 out­puts num, and check (3 : nat) out­puts nat.

We can also make definitions

definition five : num := 3 + 2

This de­clares a new con­stant five of type num to which we give the value 3 + 2. We can define func­tions with similar syntax

definition num.const₀ : num → num → num := λ x y, x -- this is a comment
-- Lean can infer types whenever they're unique
definition num.const₁                    := λ (x y : num), x
-- we can also name the arguments in the definition rather than the function body
definition num.const₂ (x y : num)        := x

The defi­ni­tion of poly­mor­phic func­tions be­comes the first point where we get a hint about what makes pro­gram­ming in de­pen­dent type the­ory differ­ent from, say, Haskell. In de­pen­dent type the­ory, the term and type lan­guages are unified, so in or­der to write a poly­mor­phic func­tion we must take the type as an ar­gu­ment.

definition poly_id (A : Type) := λ (a : A), a
-- or, equivalently
definition poly_id₁ := λ A (a : A), a
-- applied to arguments
check poly_id num 1 -- num
check poly_id (num → num → num) num.const -- num → num → num

Ex­er­cise: write a poly­mor­phic ver­sion of num.const₀.

defi­ni­tion poly_const (A B : Type) (a : A) (b : B) := a

Hav­ing to ex­plic­itly in­di­cate types ev­ery­where is a pain. In or­der to get around that, most proof as­sis­tants provide sup­port for im­plicit ar­gu­ments, which let you leave out ar­gu­ments that only have one valid value. In Lean, the syn­tax for im­plic­its looks like this:

definition id {A : Type} := λ (a : A), a

In­duc­tive types

Of course, none of this would be that use­ful if we couldn’t define new types. There are lots of ways to craft new types in de­pen­dent type the­ory, but among the most fun­da­men­tal is the cre­ation of in­duc­tive types.

To define a new in­duc­tive type, you give a list of con­struc­tor tags, each as­so­ci­ated with a type rep­re­sent­ing the ar­gu­ments it takes. The sim­plest ones are just enu­mer­a­tions. For ex­am­ple, the days of the week:

inductive weekday : Type :=
| mon : weekday
| tue : weekday
| wed : weekday
| thu : weekday
| fri : weekday
| sat : weekday
| sun : weekday

This cre­ates a new type weekday, and seven new con­stants (weekday.mon, weekday.tue,…) of type weekday. If you’re fa­mil­iar with Haskell, you’ll cor­rectly no­tice that this looks an awful lot like GADT dec­la­ra­tions.

Just like in Haskell, we can parametrize our types over other types, mak­ing new types like either:

inductive either (A B : Type) : Type :=
| inl {} : A → either A B``
| inr {} : B → either A B

From this dec­la­ra­tion, we get a new con­stant either : Type → Type → Type. This rep­re­sents the union of the types A and B, the type of val­ues that be­long ei­ther to A or B.

We can also define re­cur­sive types, such as nat­u­ral numbers

inductive nat : Type :=
| zero : nat
| succ : nat → nat

The eas­iest way to define func­tions over nats is re­cur­sively. For ex­am­ple, we can define ad­di­tion as

definition add (n : nat) : nat -> nat
| := n
| (nat.succ m) := nat.succ (add m) -- n is constant at every recursive call

Bring­ing both of these to­gether we can define the type of linked lists

inductive list (A : Type) : Type := 
| nil {} : list A
| cons : A → list A → list A

We can also define func­tions over lists by pat­tern matching

definition map {A B : Type} (f : A → B) : list A → list B
| list.nil := list.nil
| (list.cons x xs) := list.cons (f x) (map xs) -- f is constant at every recursive call

Ex­er­cise: write foldr and foldl by pat­tern matching

defi­ni­tion foldr {A B : Type} (r : A → B → B) (vnil : B) : list A → B | list.nil := vnil | (list.cons x xs) := r x (foldr xs)

definition foldl {A B : Type} (r : B → A → B) : B → list A → B :=
| b list.nil := b
| b (list.cons x xs) := foldl (r b x) xs



  • Type theory

    Modern foun­da­tions for for­mal math­e­mat­ics.