Functional Type Theory

In "Categories for Types" a functional type theory is given by the signature and axioms, just like an algebraic type theory. The difference is that the types and terms form a richer structure.

In addition to the ground types, defined just as in the last post, we have types generated by the grammar: T -> unit | a | TxT | T => T where a is a ground type. In other words, we chose our ground types and generate the set of types as the smallest set such that: all ground types are types, for all types A, B there is a type AxB (A cross B), and A -> B (functions from A to B), and the unit type is a type.

The terms are given just as before as well, with all variables as terms, all function symbols with arguments as terms, and all constants as terms, but we also have the unit term (), as well as all pairs of terms and projections for pairs, as well as lambda abstractions and applications of terms to terms.

This richer structure has additional rules to make abstraction and products work nicely. Notice that the terms are those of a lambda calculus with products with a simple type system with only function and product types. While the algebraic type theories where the language of categories with finite products, functional type theories are the language of cartisian closed categories (CCC). If you are familiar with CCCs, it should be clear that the types are objects, the products are the products of the category and the function types are the exponential objects- in other words the two constructions match up very nicely with each other.

This is a very cool thing for several reasons- first off I think it is neat that we have a logic (a type system) with a language for proofs (the existence of a term in a type proves that type and the corresponding proposition in the logic), secondly the term language is the lambda calculus (which is just awesome by itself) and thirdly it seems like CCC are the setting for computation and extract exactly the structure necessary to describe these systems of computation and logic.

I plan on posting about this subject more, and in particular I want to talk about higher order functional type theories and eventually omega lambda x hyperdoctrines (which is an awesome name) and domain theory as I learn about them.