Where can I learn about Cartesian closed functors between categories of simply typed lambda calculus?

Question

I'll try to describe the subject I am looking for literature on, or concept names that I can Google.

For each $n \geq 1$, let $\mathbf{STLC}_n$ be the category where the objects are all simply typed lambda calculus types with $n$ or fewer type variables, and the arrows are all lambda terms with the corresponding domain and codomain. For example, a Church numeral-like term (only strong enough to define composition of an arrow $a \to a$ with itself $n$ times) is a point in the type $(a \to a) \to a \to a$ in all those categories, because it has only one type variable $a$, but the object $(b \to c) \to (a \to b) \to a \to c$ (containing composition $\lambda f . \lambda g . \lambda x.f(g\ x)$ as its only point) only exists in the categories with $n \geq 3$, because there are three type variables $a$, $b$ and $c$.

These categories are Cartesian closed, so it makes sense to interpret simply typed lambda calculus in them, so that simply typed lambda calculus is interpreted over another simply typed lambda calculus. I believe this can be seen as (tuples of?) Cartesian closed functors between the categories mentioned above.

Where can I learn more about Cartesian closed functors between those categories?

I am particularly interested in their relationship with the semantics of untyped lambda calculus or some second order lambda calculus. Or do they form a Lawvere theory, or some generalization thereof?

Answer 1

If I understand correctly, you are considering simple types over $\to,\times$ as objects, $\beta$-normal, $\eta$-long $\lambda$-terms as arrows, and substitution plus normalization as composition. In that case, what you denote by $\mathbf{STLC}_n$ is the syntactic category of the simple higher-order theory with $n$ sorts and nothing else (if you prefer, the "free CCC" on a set with $n$ elements).

Now, I don't know what you mean by "simply-typed $\lambda$-calculus" but the most widespread definition is that, once you take the quotient under $\beta\eta$, this is the same thing as $\mathbf{STLC}_\omega$, that is, the "free CCC" on a countable set of atomic types $\mathcal A$. So the interpretation of the simply-typed $\lambda$-calculus in $\mathbf{STLC}_n$ is fairly uninteresting: it amounts to choosing a type $T_A$ with $n$ free atoms for every atomic type $A\in\mathcal A$, and then the interpretation of a term $t$ is the $\beta$-normal, $\eta$-long form of $t$ in which every atom $A$ is substituted with $T_A$ (typing is stable under arbitrary type substitutions). In particular, if $t$ is $\beta$-normal, $\eta$-long, then its interpretation is itself, modulo a type substitution.

It is true that this corresponds to a Cartesian-closed functor $\mathbf{STLC}_\omega\to\mathbf{STLC}_n$, but I am not sure how interesting this is. In fact, by virtue of the $\mathbf{STLC}_n$ categories being "free", any Cartesian-closed functor $\mathbf{STLC}_n\to\mathbf{STLC}_m$ amounts to choosing a type with $m$ atoms for each of the $n$ atoms of $\mathbf{STLC}_n$. That's it: the rest is imposed by the requirement that the functor be Cartesian-closed. So functors $\mathbf{STLC}_n\to\mathbf{STLC}_m$ are just finite type substitutions, restricted to types with $m$ atoms. Similarly, a Cartesian-closed functor $\mathbf{STLC}_\omega\to\mathbf{STLC}_\omega$ is an arbitrary type substition (every atom is assigned to an arbitrary simple type). It may turn out to be useful to think of type substitutions this way, although right now I don't have in mind any place where I've actually seen it done in the literature.

A relatively thorough description of the syntactic category of a simple higher-order theory may be found in vol. 2 of Johnstone's Sketches of an Elephant (otherwise simply known as "the Elephant"), section D4.2. You may learn about the general "yoga" of syntactic categories a bit earlier in the book, chapter D1 (that's about first-order theories, but the same applies to higher-order theories).