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

defi­ni­tion 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

defi­ni­tion num.const₀ : num → num → num := λ x y, x—this is a com­ment
—Lean can in­fer types when­ever they’re unique
defi­ni­tion num.const₁                    := λ (x y : num), x
—we can also name the ar­gu­ments in the defi­ni­tion rather than the func­tion body
defi­ni­tion 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.

d
efi­ni­tion poly_id (A : Type) := λ (a : A), a
—or, equiv­a­lently
defi­ni­tion poly_id₁ := λ A (a : A), a
—ap­plied to ar­gu­ments
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:

defi­ni­tion 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:

in­duc­tive week­day : Type :=
| mon : week­day
| tue : week­day
| wed : week­day
| thu : week­day
| fri : week­day
| sat : week­day
| sun : week­day

This cre­ates a new type week­day, and seven new con­stants (week­day.mon, week­day.tue, week­day.wed…) of type week­day. 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 ei­ther:

in­duc­tive ei­ther (A B : Type) : Type :=
| inl {} : A → ei­ther A B``
| inr {} : B → ei­ther A B

From this dec­la­ra­tion, we get a new con­stant ei­ther : 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

in­duc­tive 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

defi­ni­tion add (n : nat) : nat → nat
| nat.zero := n
| (nat.succ m) := nat.succ (add m) -- n is con­stant at ev­ery re­cur­sive call

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

in­duc­tive 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

defi­ni­tion 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 con­stant at ev­ery re­cur­sive 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)

defi­ni­tion 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

<div><div>

Parents:

  • Type theory

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