Faithful Ideal Models for Recursive Polymorphic Types

We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit between models and programming language. Two of our semantics of type expressions are faithful, in the sense that programs that behave identically in all contexts have exactly the same types. Keywords: Polymorphism, recursive types, full abstraction, ideals, metric models. 1. Introduction Often, a formal semantics assigns different values to programs that behave identically in all contexts [1, 2, 3]. In other words, the semantics of programming-language expressions is not fully abstract. This mismatch between model and programming language elicits diverse reactions. Some propose extensions to the programming language, while others prefer modifying the semantics. Both of these attitudes have suggested fruitful lines of research. Yet others point out that the semantics still serves its purposes ..