Types are theorems; programs are proofs

Length: 60 minutes


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