What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

Question

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 Andrej Bauer 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 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?

Answer 1

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 $A$, and consider the category of partial equivalence relations $\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.

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.