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.

Outline

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

mjd-perl-yak+@plover.com