I'm trying to draw a general mental picture about the models and the denotational semantics of the typed lambda calculus, in its different variants.
I'm particularly interested in how the semantics changes according to:
- which forms of recursion are allowed, and
- which forms of polymorphism are allowed.
I understand that, even if one makes a precise choice about these options, there are many possible models. Still, I would like to pick a few concrete examples (or even one) for each option, and draw them in my mental picture. Of course, the simplest the better. I feel that, at my current stage, I do not benefit much (yet) from abstract descriptions such as "take any such-and-such category" when I do not have any idea about how to craft at least one of those.
Since the topic is quite broad, let me ask a specific question:
What would you study next? References are welcome.
Here's what I have seen so far:
The STLC has a very simple set-theoretic model. Just interpret basic types with sets, products with cartesian products, etc. Boring but simple. Can be generalized to arbitrary CCCs.
STLC + term-level recursion / fixed points. This is essentially PCF. We can build models using CPOs ($\omega$CPOs or DCPOs or ...). They are not fully abstract, but I'm not concerned with that. To compute fixed points, Kleene's fixed point theorem saves the day.
PCF + type-level recursion. Here things start getting non-trivial. To solve type-level recursive equations, we can translate these to recursive domain equations, and solve them by lifting the Kleene $\omega$-CPO machinery at the domain level. Essentially, monotonic functions become functors, continuous functions become continuous functors, and suprema become colimits. Some issues arise since $\rightarrow$ is contravariant on its first argument, but restricting the categories at hand to embedding-projections pairs (which to me look like a special case of Galois connections) one can make everything covariant.
Adding predicative polymorphism. By this, I mean allowing types like $\prod_{\tau:\sf Mono} T(\tau)$ where $\sf Mono$ is the set of monomorphic types, which do not contain such products. In such way, the product is a countable one, hence a small one, so we can take the related product on the CPOs for monotypes without any size issues. Shallow, but simple.
Adding impredicative polymorphism, as in System F. Here $\prod_{\tau:*}$ ranges over all the types, including polymorphic ones. I'm not sure about how to proceed here. Types are still countable, but we can't simply relate to a polymorphic type $\tau'$ the product of some selected CPOs as before, since such product would also involve the CPO of $\tau'$ itself, which we are defining.
Adding dependent types. Ultimately I'd like to understand how a dependently typed semantics can be given for a language featuring unrestricted term-level recursion, and possibly type-level recursion as well. I tried to read about fibered categories, but I think I'm not yet ready to tackle those, so I'm looking for some smaller steps, first. I will try again in the future, though.
