Fri 20 Jan 2023 09:25 - 09:50 at Avenue34 - Types II Chair(s): Alan Jeffrey

In programming languages with records, objects, or traits, it is common to
have operators that allow dropping, updating or renaming some components. These operators
are useful for programmers to explicitly deal with conflicts and
override or update some components. While such operators have been
studied for record types, little work has been done to generalize and study their
theory for other types.

This paper shows that, given subtyping and disjointness relations, we
can specify and derive algorithmic implementations for
a general type difference operator that works for other types,
including function
types, record types and intersection types. When defined in this way, the type difference algebra
has many desired properties that are expected from a subtraction
operator. Together with a generic \emph{merge} operator, using type
difference we can generalize many operations on records formalized in the
literature. To illustrate the usefulness of type difference we create
an intermediate calculus with a rich set of operators on expressions of arbitrary type, and
demonstrate applications of these operators in \emph{CP}, a prototype language
for \emph{Compositional Programming}. The
semantics of the calculus is given by elaborating into a
calculus with \emph{disjoint intersection types} and a merge operator. We
have implemented type difference and all the operators % presented in this paper
in the CP language. Moreover, all the calculi and related proofs
are mechanically formalized in the Coq theorem prover.

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:15
Types IIPOPL at Avenue34
Chair(s): Alan Jeffrey Roblox
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Nick Rioux University of Pennsylvania, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Steve Zdancewic University of Pennsylvania
Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
Han Xu Peking University, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Victor Arrial Université Paris Cité - CNRS - IRIF, Giulio Guerrieri Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - Huawei, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France