Sensible Intersection Type Theories

TL;DR

This paper explores the construction of sensible filter models in intersection type theories, characterizing classes that induce models where unsolvable terms interpret as the least element, advancing the understanding of lambda-model semantics.

Contribution

It introduces a categorical framework for intersection type theories as meet-semilattices and characterizes classes that produce sensible lambda-models, including an effective class generalizing Mendler's criterion.

Findings

Identification of non-effective and effective classes of intersection type theories

Characterization of sensible filter models within these classes

Extension of Mendler's criterion to intersection types and head normalising terms

Abstract

Finitary/static semantics in the form of intersection type assignments have become a paradigm for analysing the fine structure of all sorts of lambda-models. The key step is the construction of a filter model isomorphic to a given lambda-model. A property of great interest of filter lambda-models is sensibility, i.e. the interpretation of all unsolvable terms is the least element. The flexibility of intersection type assignments derives from their parametrisation on intersection type theories. We construe intersection type theories as special meet-semilattices and show that appropriate morphisms, in the opposite category of meet-semilattices, preserve sensibility of the induced lambda-models. Interestingly the set of saturated sets together with the set of lambda-terms is such a meet-semilattice, thus showing that arguments based on Tait-Girards's computability amount to the construction of a morphism. We characterise two classes of intersection type theories which induce sensible filter models. The first is non-effective while the second is effective and it amounts to the generalisation of Mendler's criterion to intersection types and head normalising terms. The complete characterisation of sensible filter models however still escapes.