Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

Question

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied (see, e.g., Amadio & Curien, Domains and Lambda-Calculi).

H-M lies between STLC and System F, but can we find a sensible categorical model for it? Particularly, I am interested in studying type inference in this categorical framework. Can we give H-M type inference a category-theoretic specification?

This presentation by Kammar and Moss presents some ideas in this direction, but I wonder if there's more work on this, particularly work that incorporates type inference.

Answer 1

Apart from what's already written in the slides you linked to, let me describe one possible approach.

For studying type inference semantically we need a model in which a term can have many types, or none. This naturally leads to Curry-style typing, i.e., we think of $t : A$ as a relation where both the term $t$ and the type $A$ are meaningful by themselves. (The opposite is Church-style typing where a term is always formed together with its type, and it cannot stand on its own.)

We can proceed as follows:

1. Give a model of untyped terms, such as a model of the untyped $\lambda$-calculus.
2. Give a model of types.
3. Define a "has type" relation between terms and types.

A concrete well-known example of this are PER models (although they model entire System F, not just Hindley-Milner):

1. Consider any model of the untyped calculus, for example, a reflexive domain $D$.
2. The types are the partial equivalence relations on $D$ (symmetric transitive relations on $D$).
3. $t \in D$ has type $T$ when $(t,t) \ni T$.

PERs have a rich structure (they form a CCC), for instance the exponential of $S$ and $T$ is the PER $S \Rightarrow T = \{(f,g) \in D \times D \mid \forall (x,y) \in S . (f x, g y) \in T\}$. This is all well-known.

Polymorphism in this model amounts to taking intersection of partial equivalence relations. For instance, $\lambda x . x$ has type $T \Rightarrow T$ for every PER $T$, and so it also has the type $\bigcap_{X \in \mathsf{PER}(D)} (X \Rightarrow X)$, which is the interpretation of $\forall \alpha . \alpha \to \alpha$.

You'll have to find something more nuanced to capture Hindley-Milner without capturing System F. That's what Kammar and Moss set out to do.

Answer 2

This isn't an excessively deep answer, but you can express a type system based on STLC with prenex polymorphism as a Pure Type System in a quite simple way, using sorts $*_{\mathrm{mono}}$, $*_{\mathrm{poly}}$ and $\square$ along with the axioms $$ *_{\mathrm{mono}}, *_{\mathrm{poly}}\ :\ \square$$

and the rules

$$(*_{\mathrm{mono}},*_{\mathrm{mono}},*_{\mathrm{mono}}),\ (\square, *_{\mathrm{mono}}, *_{\mathrm{poly}}),\ (\square, *_{\mathrm{poly}}, *_{\mathrm{poly}}) $$

In particular, these rules allow explicit quantification over monomorphic types, without enabling the impredicative polymorphism of System F.

Now what remains is finding a categorical semantics for all (or at least sufficiently many) Pure Type Systems, and you're done!

Sadly, this is where my knowledge is lacking. Certainly, the machinery exists, either from Jacobs or even more general approaches. In this case, I suspect that some hyperdoctrine with some mild additional conditions would suffice to represent a model of the above theory.