A completeness result for a realisability semantics for an intersection type system

TL;DR

This paper introduces a realisability semantics for an intersection type system with a universal type, establishing soundness, completeness, and a correspondence between typability and inhabitance for positive types.

Contribution

It provides a novel semantics for a type system with a universal type and characterizes positive types where typability and inhabitance coincide.

Findings

Semantic interpretations are consistent across different reduction notions.

Positive types ensure terms are normalisable and reduce to closed terms.

Typability and inhabitance are equivalent for positive types.

Abstract

In this paper we consider a type system with a universal type $\omega$ where any term (whether open or closed, $\beta$-normalising or not) has type $\omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $\lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (based on weak head reduction and normal $\beta$-reduction) we obtain the same interpretation for types. Since the presence of $\omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${\mathbb U}^+$ of the so-called positive types (where $\omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $\beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${\mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${\mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${\mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties.