Paper: Applicative Intersection Types, appeared at APLAS 2022.

Also check our online Coq code, slides, conf paper, thesis and APLAS talk video.

Abstract

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. Never- theless no previous calculus supports all those features at once. In this paper 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 se- mantics 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 applica- tive dispatching relation that is used for the dynamic semantics. The two calculi and their proofs are formalized in the Coq theorem prover.

Folders

• archive/: previous (some failed) development of the formalization

• core/: a type sound calculus with applicative subtyping

• core+disjoint/: a type sound and deterministic calculus with applicative subtyping

• subtyping/: proof of sound/complete lemma of applicative subtyping with respect to (BCD) subtyping

• implementation/: interpreter and compiler in Racket, PLT Redex Mode and Haskell implementation of subtyping