Join Philly Lambda and speaker Mark Jason Dominus for another talk diving into the deep waters of type theory and the Curry-Howard correspondence. Mark writes:
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.