<p>Your description of an idealized computer is a nescient form of realizability, and there are very simple realizability models of parametric polymorphism.</p>
<p>Take a model of computatation (an &quot;idealized computer&quot;), namely <a href="https://ncatlab.org/nlab/show/partial+combinatory+algebra" rel="noreferrer">a partial combinatory algebra</a> <span class="math-container">$A$</span>, and consider the category of <a href="https://ncatlab.org/nlab/show/category+of+PERs" rel="noreferrer">partial equivalence relations</a> <span class="math-container">$\mathsf{PER}(A)$</span>. Recall that a partial equivalence relation (per) is a symmetric transitive relation <span class="math-container">$\sim$</span> on <span class="math-container">$A$</span>.</p>
<p>The intuitive idea is that the elemetns of <span class="math-container">$A$</span> are &quot;code&quot;, and pers (equivalently representations, equivalently modest sets) relate such code to abstract mathematical objects. See Section 3.1 of <a href="https://github.com/andrejbauer/notes-on-realizability/tree/master" rel="noreferrer">these notes</a>.</p>
<p>It is cartesian closed, even locally cartesian closed, and so models not only the simply typed <span class="math-container">$\lambda$</span>-calulus but also dependent types.</p>
<p>Additionally, it models System F. Given a map <span class="math-container">$F : \mathsf{PER}(A) \to \mathsf{PER}(A)$</span>, define
<span class="math-container">$$\textstyle
\forall X . F(X) =
\bigcap_{{\sim} \in \mathsf{PER}(A)} F({\sim}).
$$</span>
The model is not as good as one would wish, but is very simple to describe and is close to the intuition. For example, <span class="math-container">$\forall X . X \to X$</span> is the per, defined for <span class="math-container">$r, t \in A$</span>,
<span class="math-container">$$r \sim_{\forall X . X \to X} t \iff
 \forall {{\sim}} \in \mathsf{PER}(A) \forall {u \in A} .\, u \sim u \Rightarrow r u \sim t u.
$$</span>
By specializing <span class="math-container">$\sim$</span> to the singleton per on <span class="math-container">$u$</span>, we see that
<span class="math-container">$$
r \sim_{\forall X . X \to X} t \iff \forall u \in A.\, r u = u = t u.
$$</span>
So, the elements of <span class="math-container">$\forall X. X \to X$</span> are precisely those realizers that implement the identity map.</p>

CC BY-SA 4.0
2024-04-20T16:23:20.347Z
You say that PER categories would be intuitive and easy to map to programs, but so far I don't see that. PERs are "symmeric transitive" relations - but not reflexive, why? And they are relations on a partial combinatory algebra, what's that for?  I don't see how a System F interpreter would ever need to use such things in its code. It would take a long time to learn those abstract things.  Why not relations on sets of natural numbers, say? In the programming language, we have booleans, naturals, etc., so why aren't PERs relations on those sets?
winitzki
CC BY-SA 4.0
2024-04-20T16:36:19.143Z
I explained the intuition in the notes that I linked to, and in particular section 3.1. Modest sets described tehrein correspond directly to the programmer's intuition, and then it turns out that modest sets are equivalent to PERs. This is all explained in the notes. The advantage of PERs is that they form a small category and that polymorphism is expressed with a simple union. So I encourage you to take a look at the notes before asking further questions.
Andrej Bauer
CC BY-SA 4.0
2024-04-20T16:37:09.317Z
A System F interpreter would not know anything about PERs. It would just compute with realizers, of course. This is not uncommon: an interpreter need not be aware of the types.
Andrej Bauer
CC BY-SA 4.0
2024-04-20T15:13:11.230Z
2024-04-20T15:28:03.013Z
2024-04-20T15:28:03.013Z
Andrej Bauer
<p>In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of that language, that would correspond to how programmers actually use the language?</p>
<p>The connection to category theory would be satisfactory to programmers if, for example, the System F type <span class="math-container">$\Lambda A.~ A\to \textrm{Bool}$</span> would be shown to correspond to a contravariant functor, and the laws of that functor would correspond to equations for the <code>contramap</code> method that programmers can implement.</p>
<p>For the connection to model theory to be satisfactory from a programmer's viewpoint, the model of System F should correspond to the way that a programmer would implement an interpreter for System F. For instance, the model must be parametric: say, the System F type <span class="math-container">$\forall A.~A\to A$</span> should be inhabited only by the (polymorphic) identity function. Also, the model should somehow reflect the data structures that a programmer would clearly see as reasonable for an interpreter to use.</p>
<p>I am asking this question here because I expect this to be already known but I can't find where I could read about this.</p>
<p>Here some more details.</p>
<p>Today there are quite a few functional programming (FP) languages whose type systems are modeled after either System F or System F<span class="math-container">$\omega$</span> (usually with extensions). Practicing programmers have learned the FP idioms that are mostly features of pure System F<span class="math-container">$\omega$</span>. At some point, practicing programmers are confronted with the need to venture into category theory or model theory. Examples are when a programmer wants to implement something that looks like a lawful endofunctor and the laws need to be checked, or when a programmer wants to use parametricity-based reasoning (e.g., a function of type <span class="math-container">$\forall a.~ a\to a$</span> must be an identity function).</p>
<p>However, one often finds hand-waving reasoning about those things, instead of a rigorous presentation. For example, it is often stated that types and functions of a programming language correspond to objects and morphisms of some category; but there seems to be disagreement about how actually to define that. <a href="https://math.andrej.com/2016/08/06/hask-is-not-a-category/" rel="nofollow noreferrer">A post by Andrej Bauer</a> summarises the problems there.</p>
<p>When one tries to find sources about model theory, one finds complicated theoretical concepts (<span class="math-container">$\omega$</span>-cpo, PER categories, reflexive graph categories, etc.) that are certainly not what a programmer would expect to see.</p>
<p>For instance, a programmer would expect that the type <code>Bool</code> is modeled by a set of two values <code>True</code> and <code>False</code>, or that the function type <code>Natural</code><span class="math-container">$\to$</span><code>Natural</code> is modeled by a set of some functions from natural numbers to natural numbers. But the literature on domain theory and model theory seems to say otherwise.</p>
<p>A specific example is the <a href="https://dhall-lang.org/" rel="nofollow noreferrer">Dhall language</a> that one can view as a more or less no-frills implementation of System F<span class="math-container">$\omega$</span>. Strong normalization and termination are guaranteed. Interpreters for Dhall were written in Haskell, Java, Go, Rust, Scala, and possibly other languages. Each of these interpreters supply some kind of model for System F<span class="math-container">$\omega$</span>. But certainly none of these interpreters supply a model based on complicated mathematics that one finds in the literature. For example, a Scala-based interpreter uses straightforward recursive data types (not even GADTs) to represent terms of System F<span class="math-container">$\omega$</span> and to implement all the beta-reduction rules. There are no PER categories, reflexive graphs, or <span class="math-container">$\omega$</span>-cpos anywhere in anyone's code. Why are those things in the literature about model theory?</p>
<p>To simplify the consideration, assume that we are dealing with an idealized computer that has infinite (but countably infinite) memory, arbitrary-precision integer arithmetic, and programs can have unbounded length. In such a computer, every data structure is at most a countable set. We may write a program for that computer to implement a System F<span class="math-container">$\omega$</span> interpeter using simple data structures. That implementation will provide a model of System F<span class="math-container">$\omega$</span> that appears to be based on some structures in the idealized computer's memory; that is, a model of System F<span class="math-container">$\omega$</span> based just on some countable sets.</p>
<p>But here is a well-known paper by J. Reynolds, &quot;Polymorphism is not set-theoretic&quot;, and a well-known paper by A. Pitts, &quot;Polymorphism is set theoretic, constructively&quot;. Both papers talk about matters far removed from a programmer's experience. Neither of these papers give programmers a theoretical leg to stand on when reasoning about model theory.</p>
<p>If it is incorrect to think that types in System F / System F<span class="math-container">$\omega$</span> are just sets of some kind, what is an example of code that works incorrectly because of that mistake?</p>
<p>I have read that some models of System F / System F<span class="math-container">$\omega$</span> are non-parametric while others are parametric. But the programmers will most likely never encounter any non-parametric models while implementing an interpreter for System F<span class="math-container">$\omega$</span>. What is a realistic model for System F<span class="math-container">$\omega$</span> that programmers would recognize?</p>
<p>Similar problems occur when trying to make a connection to category theory. The problems are not even due to undefined or &quot;bottom&quot; values that Haskell has. A pure System F does not have any undefined values. Why cannot one simply say that the types and functions in System F (or System F<span class="math-container">$\omega$</span>) correspond to objects and morphisms of a certain category? If this is not true, what code written in System F would run incorrectly due to that mistake?</p>

CC BY-SA 4.0
2024-04-20T14:57:10.567Z
An obvious model that fits closely with how programmers' intuitions works are PER models. Don't those fit the bill? In fact, your description of idealized computer is a nescient form of a realizability model.
Andrej Bauer
CC BY-SA 4.0
2024-04-20T17:02:53.807Z
Why do working Haskell programmers talk about "bottom" and "strictness," which are domain theoretic concepts? Many of them can probably also explain to you how the latter does not correspond naively to some operational evaluation order. Apparently their code does contain DCPOs.
Dan Doel
CC BY-SA 4.0
2024-04-20T19:04:47.997Z
@DanDoel Haskell code looks like `x = y` or some lambda terms, type constructors, and so on. It doesn't look anything like the arcane stuff one finds in books and papers on domain theory. Of course, I agree that bottom and strictness are important and nontrivial concepts. But I specifically chose to talk about System F and System F$\omega$ because those systems are strongly normalizing and we don't need to confront bottom or strictness while staying within those systems.
winitzki
<type-theory><ct.category-theory><typed-lambda-calculus><denotational-semantics><model-theory>
What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?
winitzki
# What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

(Asked by: username_0 on 2024-04-20)

In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of that language, that would correspond to how programmers actually use the language?

The connection to category theory would be satisfactory to programmers if, for example, the System F type $\Lambda A.~ A\to \textrm{Bool}$ would be shown to correspond to a contravariant functor, and the laws of that functor would correspond to equations for the `contramap` method that programmers can implement.

For the connection to model theory to be satisfactory from a programmer's viewpoint, the model of System F should correspond to the way that a programmer would implement an interpreter for System F. For instance, the model must be parametric: say, the System F type $\forall A.~A\to A$ should be inhabited only by the (polymorphic) identity function. Also, the model should somehow reflect the data structures that a programmer would clearly see as reasonable for an interpreter to use.

I am asking this question here because I expect this to be already known but I can't find where I could read about this.

Here some more details.

Today there are quite a few functional programming (FP) languages whose type systems are modeled after either System F or System F$\omega$ (usually with extensions). Practicing programmers have learned the FP idioms that are mostly features of pure System F$\omega$. At some point, practicing programmers are confronted with the need to venture into category theory or model theory. Examples are when a programmer wants to implement something that looks like a lawful endofunctor and the laws need to be checked, or when a programmer wants to use parametricity-based reasoning (e.g., a function of type $\forall a.~ a\to a$ must be an identity function).

However, one often finds hand-waving reasoning about those things, instead of a rigorous presentation. For example, it is often stated that types and functions of a programming language correspond to objects and morphisms of some category; but there seems to be disagreement about how actually to define that. [A post by username_1](https://math.andrej.com/2016/08/06/hask-is-not-a-category/) summarises the problems there.

When one tries to find sources about model theory, one finds complicated theoretical concepts ($\omega$-cpo, PER categories, reflexive graph categories, etc.) that are certainly not what a programmer would expect to see.

For instance, a programmer would expect that the type `Bool` is modeled by a set of two values `True` and `False`, or that the function type `Natural`$\to$`Natural` is modeled by a set of some functions from natural numbers to natural numbers. But the literature on domain theory and model theory seems to say otherwise.

A specific example is the [Dhall language](https://dhall-lang.org/) that one can view as a more or less no-frills implementation of System F$\omega$. Strong normalization and termination are guaranteed. Interpreters for Dhall were written in Haskell, Java, Go, Rust, Scala, and possibly other languages. Each of these interpreters supply some kind of model for System F$\omega$. But certainly none of these interpreters supply a model based on complicated mathematics that one finds in the literature. For example, a Scala-based interpreter uses straightforward recursive data types (not even GADTs) to represent terms of System F$\omega$ and to implement all the beta-reduction rules. There are no PER categories, reflexive graphs, or $\omega$-cpos anywhere in anyone's code. Why are those things in the literature about model theory?

To simplify the consideration, assume that we are dealing with an idealized computer that has infinite (but countably infinite) memory, arbitrary-precision integer arithmetic, and programs can have unbounded length. In such a computer, every data structure is at most a countable set. We may write a program for that computer to implement a System F$\omega$ interpeter using simple data structures. That implementation will provide a model of System F$\omega$ that appears to be based on some structures in the idealized computer's memory; that is, a model of System F$\omega$ based just on some countable sets.

But here is a well-known paper by J. Reynolds, "Polymorphism is not set-theoretic", and a well-known paper by A. Pitts, "Polymorphism is set theoretic, constructively". Both papers talk about matters far removed from a programmer's experience. Neither of these papers give programmers a theoretical leg to stand on when reasoning about model theory.

If it is incorrect to think that types in System F / System F$\omega$ are just sets of some kind, what is an example of code that works incorrectly because of that mistake?

I have read that some models of System F / System F$\omega$ are non-parametric while others are parametric. But the programmers will most likely never encounter any non-parametric models while implementing an interpreter for System F$\omega$. What is a realistic model for System F$\omega$ that programmers would recognize?

Similar problems occur when trying to make a connection to category theory. The problems are not even due to undefined or "bottom" values that Haskell has. A pure System F does not have any undefined values. Why cannot one simply say that the types and functions in System F (or System F$\omega$) correspond to objects and morphisms of a certain category? If this is not true, what code written in System F would run incorrectly due to that mistake?

**Tags:** type-theory, ct.category-theory, typed-lambda-calculus, denotational-semantics, model-theory

> **Comments:**
> **username_1**: An obvious model that fits closely with how programmers' intuitions works are PER models. Don't those fit the bill? In fact, your description of idealized computer is a nescient form of a realizability model.  
> **username_2**: Why do working Haskell programmers talk about "bottom" and "strictness," which are domain theoretic concepts? Many of them can probably also explain to you how the latter does not correspond naively to some operational evaluation order. Apparently their code does contain DCPOs.  
> **username_0**: @DanDoel Haskell code looks like `x = y` or some lambda terms, type constructors, and so on. It doesn't look anything like the arcane stuff one finds in books and papers on domain theory. Of course, I agree that bottom and strictness are important and nontrivial concepts. But I specifically chose to talk about System F and System F$\omega$ because those systems are strongly normalizing and we don't need to confront bottom or strictness while staying within those systems.  

---

## 1 answers

### Answer by username_1 on 2024-04-20. Score: 5

Your description of an idealized computer is a nescient form of realizability, and there are very simple realizability models of parametric polymorphism.

Take a model of computatation (an "idealized computer"), namely [a partial combinatory algebra](https://ncatlab.org/nlab/show/partial+combinatory+algebra) $A$, and consider the category of [partial equivalence relations](https://ncatlab.org/nlab/show/category+of+PERs) $\mathsf{PER}(A)$. Recall that a partial equivalence relation (per) is a symmetric transitive relation $\sim$ on $A$.

The intuitive idea is that the elemetns of $A$ are "code", and pers (equivalently representations, equivalently modest sets) relate such code to abstract mathematical objects. See Section 3.1 of [these notes](https://github.com/andrejbauer/notes-on-realizability/tree/master).

It is cartesian closed, even locally cartesian closed, and so models not only the simply typed $\lambda$-calulus but also dependent types.

Additionally, it models System F. Given a map $F : \mathsf{PER}(A) \to \mathsf{PER}(A)$, define
$$\textstyle
\forall X . F(X) =
\bigcap\_{{\sim} \in \mathsf{PER}(A)} F({\sim}).
$$
The model is not as good as one would wish, but is very simple to describe and is close to the intuition. For example, $\forall X . X \to X$ is the per, defined for $r, t \in A$,
$$r \sim\_{\forall X . X \to X} t \iff
\forall {{\sim}} \in \mathsf{PER}(A) \forall {u \in A} .\, u \sim u \Rightarrow r u \sim t u.
$$
By specializing $\sim$ to the singleton per on $u$, we see that
$$
r \sim\_{\forall X . X \to X} t \iff \forall u \in A.\, r u = u = t u.
$$
So, the elements of $\forall X. X \to X$ are precisely those realizers that implement the identity map.

> **Comments:**
> **username_0**: You say that PER categories would be intuitive and easy to map to programs, but so far I don't see that. PERs are "symmeric transitive" relations - but not reflexive, why? And they are relations on a partial combinatory algebra, what's that for?  I don't see how a System F interpreter would ever need to use such things in its code. It would take a long time to learn those abstract things.  Why not relations on sets of natural numbers, say? In the programming language, we have booleans, naturals, etc., so why aren't PERs relations on those sets?  
> **username_1**: I explained the intuition in the notes that I linked to, and in particular section 3.1. Modest sets described tehrein correspond directly to the programmer's intuition, and then it turns out that modest sets are equivalent to PERs. This is all explained in the notes. The advantage of PERs is that they form a small category and that polymorphism is expressed with a simple union. So I encourage you to take a look at the notes before asking further questions.  
> **username_1**: A System F interpreter would not know anything about PERs. It would just compute with realizers, of course. This is not uncommon: an interpreter need not be aware of the types.  

---

