To pozorvlak

[ryani]

To pozorvlak:

Can you please explain the section "Categorical Models of Type Theory" in the wikipedia entry on Intuitionistic Type Theory?

I understand (most) of the words on their own, but the sentences seem to just stop making sense to me as I read it.

Comments

[pozorvlak]

Hmmmm... It doesn't make a lot of sense, does it? I'll have to think about this, but I think the basic idea is that you have a category C, whose objects you call "contexts", and to each context you assign a set of terms, indexed by a set of types (in other words, a family of sets of terms). This assignment is functorial (and contravariant) so it plays nicely with substitution (of variables, presumably). Depending on which kind of logic we want our type theory to be isomorphic to, we impose various extra axioms on our category of contexts and on our functor T : C^op -> Fam(Set), saying that they're closed under various forms of product and so on.

Does that help at all?

Aha!

[ryani]

Yes, that helps a bit. Also, I was just reading a paper by John Hughes about arrows and he has a description on page 51 that made a lot more sense:

However, as we saw in the introduction, there is little interesting that can be done without more operations on arrows than just composition. The same is true in category theory, and mathematicians have explored an extensive flora of additional operations that some categories have. Of particular interest to programming language semanticists are cartesian closed categories, which have just the right structure to model λ-calculus. In such models, the meaning of a λ-expression is an arrow of the category, from the types of its free variables (the context), to the type of its value [...]

Re: Aha!

[pozorvlak]

Yep. This is all an example of the Curry-Howard Isomorphism. The essential idea is that type systems correspond to logics of various strengths. On one side, we have our familiar categories whose objects are types and whose morphisms are functions. On the other side, we have categories whose objects are formulae in some logical language ("(p and q) implies (p or q)", for instance), and whose morphisms from X to Y are proofs that X implies Y. Curry and Howard observed that, for the categories of proofs that arose from intuitionistic propositional logic (no quantifiers, no (?) excluded middle), there were isomorphisms to categories that arose from simply-typed lambda calculus (there's more than one category because you can choose different sets of basic variables and, more significantly, different rules of inference). The relevant categories here are cartesian closed, which means that they have finite products and exponentials: for instance, Hask is cartesian closed, with products being tuple types and exponentials being function types

[jccw]

I think the problem with this wikipedia entry is that it's trying to summarize in a few paragraph something that you really need a book or two to really explain.

[pozorvlak]

Sure, but it also has the hallmarks of an author who's less interested in explaining the material than in demonstrating how clever he is...