Modular Inference of Linear Types for Multiplicity-Annotated Arrows

TL;DR

This paper introduces a formal inference system for a linear type system with multiplicity annotations, enabling principal type inference and addressing ambiguity issues in higher-order functions.

Contribution

It formalizes a principal type inference algorithm for a linear type system with multiplicity annotations, based on OutsideIn(X), improving inference reliability.

Findings

The proposed system infers principal types for a rank 1 qualified-typed linear calculus.

Quantifier elimination effectively resolves type ambiguity issues.

The approach demonstrates practical applicability through illustrative examples.

Abstract

Bernardy et al. [2018] proposed a linear type system $\lambda^q_\to$ as a core type system of Linear Haskell. In the system, linearity is represented by annotated arrow types $A \to_m B$, where $m$ denotes the multiplicity of the argument. Thanks to this representation, existing non-linear code typechecks as it is, and newly written linear code can be used with existing non-linear code in many cases. However, little is known about the type inference of $\lambda^q_\to$. Although the Linear Haskell implementation is equipped with type inference, its algorithm has not been formalized, and the implementation often fails to infer principal types, especially for higher-order functions. In this paper, based on OutsideIn(X) [Vytiniotis et al., 2011], we propose an inference system for a rank 1 qualified-typed variant of $\lambda^q_\to$, which infers principal types. A technical challenge in this new setting is to deal with ambiguous types inferred by naive qualified typing. We address this ambiguity issue through quantifier elimination and demonstrate the effectiveness of the approach with examples.