dependent types

logical verification week 8 2004 11 03

where are we?

Curry-Howard-de Bruijn continued

propositional logic ↔ simple type theory

λ→

predicate logic ↔ type theory with dependent types

λP

2nd order propositional logic ↔ polymorphic type theory

λ2

Barendregt’s lambda cube

[figure: λω; λC; λ2; polymorphism; λP 2; λ\underline{ω}; λP \underline{ω}; λ→; dependence; λP]

recap predicate logic

syntax

terms_{• f(M_{1}, …, M_{n})}_{• x} formulas

• P (M_{1}, …, M_{n})

• ⊤

• ⊥

• ¬A

• A → B

• A ∧ B

• A ∨ B

• ∀x. A
• ∃x. A

rules

introduction rules  elimination rules

I⊤

E⊥
I[x]¬  E¬
I[x]→  E→
I∧  El ∧ Er∧
Il ∨ Ir∨  E∨
I∀  E∀
I∃  E∃

example_{(∀x. P (x)) → ¬∃y. ¬P (y)}

5

dependent types

natlist
Inductive natlist : Set :=
nil : natlist
| cons : nat -> natlist -> natlist.

append & reverse
Fixpoint append (k l : natlist) {struct k} : natlist :=
match k with
  nil => l
| cons h t => cons h (append t l)
end.
Fixpoint reverse (k : natlist) : natlist :=
match k with
  nil => nil
| cons h t => append (reverse t) (cons h nil)
end.

lists of a given length

Fixpoint zeroes (n : nat) : natlist :=
match n with
O => nil
| S n' => cons 0 (zeroes n')
end.

0 ↦
1 ↦ 0
2 ↦ 0, 0
3 ↦ 0, 0, 0
4 ↦ 0, 0, 0, 0

dependent lists

we will define a type for lists of a given length

                          a : (natlist_dep 6)

this corresponds in normal programming languages to something like

                      int a[6]

the type of a is called a dependent type it depends on the natural number 6

                natlist_dep : nat -> Set
              natlist_dep 6 : Set

natlist_dep
Inductive natlist_dep : nat -> Set :=
    nil : natlist_dep O
  | cons : forall n : nat,
      nat -> natlist_dep n -> natlist_dep (S n).

3, 1, 4, 1, 5, 9
↓

cons 5 3 (cons 4 1 (cons 3 4 (cons 2 1 (cons 1 5 (cons 0 9 nil))))
                                                : (natlist_dep 6)

zeroes for dependent lists

Fixpoint zeroes (n : nat) : natlist_dep n :=
match n return natlist_dep n with
  O => nil
| S n' => cons n' O (zeroes n')
end.

the type of dependent zeroes

zeroes : nat -> natlist_dep ?
zeroes : forall n : nat, natlist_dep n

dependent product generalizes the notion of function type

function types and dependent products

A → B ↓ Πx : A. B

                          A -> B

↓

                     forall x : A, B

append for dependent lists

Fixpoint append (n m : nat)
(k : natlist_dep n) (l : natlist_dep m) {struct k} :
  natlist_dep (plus n m) :=
match k
  in natlist_dep n return natlist_dep (plus n m)
with
  nil => l
| cons n' h t => cons (plus n' m) h (append n' m t l)
end.

reverse for dependent lists

Fixpoint reverse
(n : nat) (k : natlist_dep n) {struct k} :
  natlist_dep n :=
match k in natlist_dep n return natlist_dep n with
  nil => nil
| cons n' h t =>
    eq_rec (plus n' 1) (fun n => natlist_dep n)
      (append n' 1 (reverse n' t) (cons 0 h nil))
      (S n') (plus_one n')
end.
has type natlist_dep (plus n' 1)

but should have type natlist_dep (S n')

reduction of dependent types

append nil l : natlist_dep (plus O m)

↓ ↓_{βδι}

           l : natlist_dep m

equality and dependent types

reverse (cons n' h t) : natlist_dep (S n')

is not interchangable with

append (reverse n' t) : natlist_dep (plus n' 1)

       (cons 0 h nil)

Curry-Howard-de Bruijn for predicate logic

Brouwer-Heyting-Kolmogorov for implication

proof of A → B is defined to be

function that maps proofs of A to proofs of B

Brouwer-Heyting-Kolmogorov for universal quantification

proof of ∀x. P (x) is defined to be

function that maps objects x to proofs of P (x)

the proper type system λP

unification of terms and types

λ→  terms and types are separate worlds
λx. x
A → B
λP  terms and types are the same kind of expression
λx. A → B

syntax

• variables x, y, z, …

• lambda abstraction λx : M. N

• function application MN

• dependent product Πx : M. N

• two ‘sorts’ ∗ and □

rules_{next week}

22

different notations for dependent products

syntactic alternatives

Πx : M. N
∀x : M. N

just different ways of writing exactly the same term

coq syntax

                      forall x : M, N

Prop, Set and Type in λP

Prop → ∗
 Set → ∗
Type → □

Prop : Type → ∗ : □
Set : Type → ∗ : □

terms and formulas of minimal predicate logic in λP

\begin{aligned}f(M_{1}, …, M_{n}) & → & fM_{1} … M_{n} \\ x & → & x \\ P (M_{1}, …, M_{n}) & → & P M_{1} … M_{n} \\ A → B & → & Πu : A. B \\ ∀x.A & → & Πx : Terms. A \end{aligned}

where

           Terms : ∗
              f : Πx_{1} : Terms. . . . Πx_{n} : Terms. Terms

P : Πx_{1} : Terms. … Πx_{n} : Terms. ∗

proofs in λP: implication

\frac{[A^{u}] ; ⋮ ; B}{A → B} I[u]→  λu : A. M : Πu : A. B

with M : B

\frac{⋮ ; A → B  ⋮ ; A}{B} E→  MN : B

with M : Πu : A. B N : A

proofs in λP: universal quantification

\frac{⋮ ; A}{∀x. A} I∀ λx : Terms. M : Πx : Terms. A

with M : A

\frac{⋮ ; ∀x. A}{A[x := N]} E∀ MN : A[x := N]

with M : Πx : Terms. A

      N : Terms

examples

example 1

∀x. (P (x) → (∀y. P (y) → A) → A)

example 2_{(∀x. P (x) → Q(x)) → (∀x. P (x)) → ∀y. Q(y)}

29

dependent types in programming

printf

what is the type of printf?

printf("hello\n")
printf("%d\n", 3)
printf(s, . . . )
printf : string → unit
printf : string → int → unit
printf : Πs : string . printftype s
printftype : string → Set

printftype
Fixpoint printftype (s : string) : Set :=
match s with
  nil => unit
| cons '%' (cons 'd' t) => int -> printftype t
| cons '%' (cons 'c' t) => char -> printftype t
| cons '%' (cons 'f' t) => float -> printftype t
| cons '%' (cons 's' t) => string -> printftype t

| …

| cons _t => printftype t
end.

dependently typed functional programming languages

• cayenne ‘dependent haskell’ Lennart Augustsson

• dependent ML Hongwei Xi

• epigram Conor McBride

the religion of dependent types

Why do dependent types matter? Types matter. That’s what they’re for – to classify data with respect to criteria which matter: how they should be stored in memory, whether they can be safely passed as inputs to a given operation, even who is allowed to see them. Dependent types are types expressed in terms of data, explicitly relating their inhabitants to that data. As such, they enable you to express more of what matters about data. Dependent types are better at mattering on your behalf, and that is why I hope they might matter to you.

– Conor McBride

summary

the three main things we have seen today

• dependent types in programming

• generalizing function types to dependent products

A → B

↓
Πx : A. B

• Curry-Howard-de Bruijn for predicate logic