Typed Lambda Calculus models and denotations

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:

1. which forms of recursion are allowed, and
2. 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.

• PER models seem like a natural next thing to study. – Andrej Bauer Aug 29 '16 at 13:01
• @chi, what do you count as denotational semantics? – Martin Berger Aug 29 '16 at 15:46
• @MartinBerger Good point. I guess I have a bias towards domain-theoretic semantics (à la Winskel's book) since I want to handle non-termination. I'm also willing to explore set-theoretical models for some terminating fragment, especially if they can be extended to cover non-termination as well. I'm not much familiar on those at the moment, though. – chi Aug 29 '16 at 16:44
• @chi How about logical formulae ordered by implication? – Martin Berger Aug 29 '16 at 17:31
• Maybe Paul Taylor's Appendix A of paultaylor.eu/stable/prot.pdf, that's a classic. If you want to dive into category theory you could try the recent paper by Ghani, Nordvall and Simpson (link.springer.com/chapter/10.1007%2F978-3-662-49630-5_1 or pure.strath.ac.uk/portal/en/publications/… for a pdf) – Andrej Bauer Aug 30 '16 at 12:16