Algebraic and Functional Type Theory

I've been reading "Categories for Types" for months now, and I'm finally starting to really get it. This book is great by the way- it goes over the theory of lattices, domains, posets, and categories (where it gets all the way from "what is a category" to the yoneda lemma and cartisian closed categories) before getting into type theory.

There is a chapter on algebraic type theory that goes over how to specify an algebraic theory as a syntactic system before giving it a meaning in some category. We do this in the lambda calculus, and it is a formal language and things like reductions are equivalences that we induce over words in the language so that computing equivalences tells us something in the semantics we have in mind. The fact that this is true in algebraic theories is new to me and very neat.

For example, the theory of groups is normally given by (S, +, 0, -), in additive notation, such that S is a set, + : SxS -> S, -: S -> s, 0 in S. In addition we have the axioms that make this structure into a group- let and right sided identity for 0, closure under +, the existence of inverse for all elements, and the associativity of +.

This data given as a type theory goes a little differently. First we define the Theory as a signature and its axioms. The signature has the types, in this case just the one type S, and the function symbols, their arities, and their sortings. The symbols are +, -, and e (the identity) with arities 2, 1, 0 respectively. The sorting says which arguments to the function have which types, but their is only one type here so that is pretty clear.

The axioms are a set of "equations in context". A context is of the form [(xi,Ti)], a list of variables paired with their type. Using |- for the turnstile symbol, the axioms look like "x:S, y:S, z:S |- (x+y)+z = x+(y+z):G" which is an equality of terms using the function symbol + (obviously this is the associative axiom. The theorems of the theory are the things that can be proven with the axioms and the rules for deriving true statements. Clearly all the axioms are theorems, as well as many other statements. When modeling a theory it is important to consider if the theorems of the theory are true in the model (soundness) and if the things true in (all of ) the models are present in the theory (completeness).

With this theory now given syntactically we can interpret it by giving it models as collections of objects and morphisms in a category. I will post more about this as I learn it because I think it is just incredibly interesting. This is just great material.