Formalizing Box Inference for Capture Calculus

TL;DR

This paper formalizes box inference in capture calculus to reduce notational complexity and enable effective effect checking in programming languages, ensuring soundness and completeness.

Contribution

It introduces a formal system for inferring boxes in capture calculus, including a semi-algorithmic variant and a type-level inference system with proven soundness and completeness.

Findings

Developed a semi-algorithmic capture calculus variant.

Derived an inference system for missing box operations.

Proved the soundness and completeness of the inference methods.

Abstract

Capture calculus has recently been proposed as a solution to effect checking, achieved by tracking the captured references of terms in the types. Boxes, along with the box and unbox operations, are a crucial construct in capture calculus, which maintains the hygiene of types and improves the expressiveness of polymorphism over capturing types. Despite their usefulness in the formalism, boxes would soon become a heavy notational burden for users when the program grows. It thus necessitates the inference of boxes when integrating capture checking into a mainstream programming language. In this paper, we develop a formalisation of box inference for capture calculus. We begin by introducing a semi-algorithmic variant of the capture calculus, from which we derive an inference system where typed transformations are applied to complete missing box operations in programs. Then, we propose a type-level system that performs provably equivalent inference on the type level, without actually transforming the program. In the metatheory, we establish the relationships between these systems and capture calculus, thereby proving both the soundness and the completeness of box inference.