Length: 60 minutes
a -> (b -> b) a -> (b -> a) a -> (a -> b) -> bbut it is impossible to construct functions with types
a -> (a -> b) (a -> b) -> a (a -> b) -> bWhat 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 Talksmjdemail@example.com