References & Citations
Computer Science > Programming Languages
Title: Modular Inference of Linear Types for Multiplicity-Annotated Arrows
(Submitted on 1 Nov 2019 (v1), last revised 19 Feb 2020 (this version, v2))
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.
Submission history
From: Kazutaka Matsuda [view email][v1] Fri, 1 Nov 2019 09:06:46 GMT (52kb)
[v2] Wed, 19 Feb 2020 05:26:18 GMT (55kb)
Link back to: arXiv, form interface, contact.