Applicative intersection types

Abstract

A new programming language is often elaborated by introducing different features. Some of those features are not orthogonal, and their combination risks breaking the safety of the whole system, especially in statically typed languages. Also, the newly coming feature is conventionally reasoned in isolation or in a rather minimised calculus. It is not surprising for language researchers and implementers to desire a general framework that contains features as much as possible and has salient extensibility. Intersection types are a nice fit for this purpose.

Calculi with intersection types have been used over the years to model various features, including: overloading, extensible records and, more recently, nested composition and return type overloading. Nevertheless, no previous calculus supports all those features at once.

In this thesis, we study expressive calculi with intersection types and a merge operator. Our first calculus supports an unrestricted merge operator, which is able to support all the features, and is proven to be type sound. However, the semantics is non-deterministic. In the second calculus we employ a previously proposed disjointness restriction, to make the semantics deterministic. Some forms of overloading are forbidden, but all other features are supported.

The main challenge in the design is related to the semantics of applications and record projections. We propose an applicative subtyping relation that enables the inference of result types for applications and projections. Correspondingly, there is an applicative dispatching relation that is used for the dynamic semantics. The two calculi and their proofs are formalised in the Coq theorem prover and we have a prototype implementation as well.