<p>This isn't an excessively deep answer, but you can express a type system based on STLC with prenex polymorphism as a <a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="noreferrer"><em>Pure Type System</em></a> in a quite simple way, using sorts <span class="math-container">$*_{\mathrm{mono}}$</span>, <span class="math-container">$*_{\mathrm{poly}}$</span> and <span class="math-container">$\square$</span> along with the axioms
<span class="math-container">$$ *_{\mathrm{mono}}, *_{\mathrm{poly}}\ :\ \square$$</span></p>
<p>and the rules</p>
<p><span class="math-container">$$(*_{\mathrm{mono}},*_{\mathrm{mono}},*_{\mathrm{mono}}),\ (\square, *_{\mathrm{mono}}, *_{\mathrm{poly}}),\ (\square, *_{\mathrm{poly}}, *_{\mathrm{poly}}) $$</span></p>
<p>In particular, these rules allow explicit quantification over monomorphic types, without enabling the impredicative polymorphism of System F.</p>
<p>Now what remains is finding a categorical semantics for all (or at least sufficiently many) Pure Type Systems, and you're done!</p>
<p>Sadly, this is where my knowledge is lacking. Certainly, the machinery exists, either from <a href="http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html" rel="noreferrer">Jacobs</a> or even <a href="https://ncatlab.org/nlab/show/categorical+model+of+dependent+types" rel="noreferrer">more general approaches</a>. In this case, I suspect that some <a href="https://ncatlab.org/nlab/show/hyperdoctrine" rel="noreferrer">hyperdoctrine</a> with some mild additional conditions would suffice to represent a model of the above theory.</p>

CC BY-SA 4.0
2020-07-28T12:52:53.357Z
2020-07-28T12:52:53.357Z
cody
<p>Apart from what's already written in the slides you linked to, let me describe one possible approach.</p>
<p>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 <span class="math-container">$t : A$</span> as a relation where both the term <span class="math-container">$t$</span> and the type <span class="math-container">$A$</span> 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.)</p>
<p>We can proceed as follows:</p>
<ol>
<li>Give a model of untyped terms, such as a model of the untyped <span class="math-container">$\lambda$</span>-calculus.</li>
<li>Give a model of types.</li>
<li>Define a &quot;has type&quot; relation between terms and types.</li>
</ol>
<p>A concrete well-known example of this are PER models (although they model entire System F, not just Hindley-Milner):</p>
<ol>
<li>Consider any model of the untyped calculus, for example, a reflexive domain <span class="math-container">$D$</span>.</li>
<li>The types are the partial equivalence relations on <span class="math-container">$D$</span> (symmetric transitive relations on <span class="math-container">$D$</span>).</li>
<li><span class="math-container">$t \in D$</span> has type <span class="math-container">$T$</span> when <span class="math-container">$(t,t) \ni T$</span>.</li>
</ol>
<p>PERs have a rich structure (they form a CCC), for instance the exponential of <span class="math-container">$S$</span> and <span class="math-container">$T$</span> is the PER <span class="math-container">$S \Rightarrow T = \{(f,g) \in D \times D \mid \forall (x,y) \in S . (f x, g y) \in T\}$</span>. This is all well-known.</p>
<p>Polymorphism in this model amounts to taking intersection of partial equivalence relations. For instance, <span class="math-container">$\lambda x . x$</span> has type <span class="math-container">$T \Rightarrow T$</span> for every PER <span class="math-container">$T$</span>, and so it also has the type <span class="math-container">$\bigcap_{X \in \mathsf{PER}(D)} (X \Rightarrow X)$</span>, which is the interpretation of <span class="math-container">$\forall \alpha . \alpha \to \alpha$</span>.</p>
<p>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.</p>

CC BY-SA 4.0
2020-07-26T11:24:38.007Z
2020-07-27T09:37:13.507Z
2020-07-27T09:37:13.507Z
Andrej Bauer
<p>It is well known that any CCC (cartesian closed category) is a model of the simply-typed <span class="math-container">$\lambda$</span>-calculus. It is less well known that System F admits a categorical model, but it is also well studied (see, e.g., Amadio &amp; Curien, <em>Domains and Lambda-Calculi</em>).</p>
<p>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?</p>
<p>This <a href="http://denotational.co.uk/talks/kammar-moss-hope-a-den-sem-for-hm-poly.pdf" rel="noreferrer">presentation</a> 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.</p>

<pl.programming-languages><ct.category-theory><type-systems><type-inference>
Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?
xrq
# Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

(Asked by: username_0 on 2020-07-25)

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](http://denotational.co.uk/talks/kammar-moss-hope-a-den-sem-for-hm-poly.pdf) 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.

**Tags:** pl.programming-languages, ct.category-theory, type-systems, type-inference

---

## 2 answers

### Answer by username_1 on 2020-07-28. Score: 5

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*](https://en.wikipedia.org/wiki/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](http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html) or even [more general approaches](https://ncatlab.org/nlab/show/categorical+model+of+dependent+types). In this case, I suspect that some [hyperdoctrine](https://ncatlab.org/nlab/show/hyperdoctrine) with some mild additional conditions would suffice to represent a model of the above theory.


---

### Answer by username_2 on 2020-07-26. Score: 5

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.


---

