Applicative Intersection Types
Calculi with intersection types have been used over the years to model various features, including: \emph{overloading}, \emph{extensible records} and, more recently, \emph{nested composition} and \emph{return type overloading}. Nevertheless 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 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 formalized in the Coq theorem prover.
Mon 5 DecDisplayed time zone: Auckland, Wellington change
15:30 - 17:30 | |||
15:30 30mTalk | Characterizing functions mappable over GADTs APLAS | ||
16:00 30mTalk | Applicative Intersection Types APLAS Xu Xue University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Ningning Xie University of Toronto | ||
16:30 30mTalk | A Calculus with Recursive Types, Record Concatenation and Subtyping APLAS Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Andong Fan Hong Kong University of Science and Technology | ||
17:00 30mTalk | Novice Type Error Diagnosis with Natural Language Models APLAS Chuqin Geng McGill University, Haolin Ye McGill University, Yixuan Li McGill University, Tianyu Han McGill University, Brigitte Pientka McGill University, Xujie Si McGill University, Canada |