# Types are theorems; programs are proofs

**Length:** 60 minutes

## Description

One of the most famous features of functional languages such as
Haskell and Scala is their complex, fine-grained type systems. In
Haskell, we find that it's easy to construct functions with types
a -> (b -> b)
a -> (b -> a)
a -> (a -> b) -> b

but it is impossible to construct functions with types
a -> (a -> b)
(a -> b) -> a
(a -> b) -> b

What is the distinction here? The answer is astounding:

There is a function of type *T* if and only if *T*,
reinterpreted as a statement of logic,
is a *true* statement.

The correspondence goes futher: if you have a program *P* with type *T*,
then not only can you understand *T* as a theorem of logic, but you can
understand *P* as a proof of the theorem. Or working the other way, if
you have a proof *P* of some logical theorem *T*, you can convert *P* into a
program whose type is *T*.
This is the foundation for more complex, dependently-typed languages
such as Agda where the type of a program *P* are understood explicitly
as assertions about the behavior of *P*.

Return to:
Universe of Discourse main page |
Perl Paraphernalia |
Other Classes and Talks

mjd-perl-yak+@plover.com