TY - GEN
T1 - Modular Inference of Linear Types for Multiplicity-Annotated Arrows
AU - Matsuda, Kazutaka
N1 - Funding Information:
We thank Meng Wang, Atsushi Igarashi, and the anonymous reviewers of ESOP 2020 for their helpful comments on the preliminary versions of this paper. This work was partially supported by JSPS KAKENHI Grant Numbers 15H02681 and 19K11892, JSPS Bilateral Program, Grant Number JPJSBP120199913, the Kayamori Foundation of Informational Science Advancement, and EPSRC Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EP/T008911/1).
Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - Bernardy et al. [2018] proposed a linear type system as a core type system of Linear Haskell. In the system, linearity is represented by annotated arrow types, 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. 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, 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.
AB - Bernardy et al. [2018] proposed a linear type system as a core type system of Linear Haskell. In the system, linearity is represented by annotated arrow types, 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. 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, 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.
KW - Linear Types
KW - Qualified Typing
KW - Type Inference
UR - http://www.scopus.com/inward/record.url?scp=85083972594&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85083972594&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-44914-8_17
DO - 10.1007/978-3-030-44914-8_17
M3 - Conference contribution
AN - SCOPUS:85083972594
SN - 9783030449131
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 456
EP - 483
BT - Programming Languages and Systems- 29th European Symposium on Programming, ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
A2 - Müller, Peter
PB - Springer
T2 - 29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Y2 - 25 April 2020 through 30 April 2020
ER -