Modular Inference of Linear Types for Multiplicity-Annotated Arrows
Modular Inference of Linear Types for Multiplicity-Annotated Arrows
复制标题
DOI：
10.1007/978-3-030-44914-8_17
复制
发表时间：
2020-04-18
期刊：
影响因子：
--
通讯作者：
Matsuda K
中科院分区：
文献类型：
--
作者：
Matsuda K
Bernardy等。 [2018]提出了一个线性类型系统作为线性haskell的核心类型系统。在系统中，线性性用注释的箭头类型表示，其中m表示参数的多重性。借助此表示，现有的非线性代码类型是原样，在许多情况下，新编写的线性代码可以与现有的非线性代码一起使用。但是，关于类型的推断知之甚少。尽管线性Haskell实现配备了类型推理，但其算法尚未正式化，并且该实现通常无法推断主要类型，尤其是对于高阶功能。在本文中，基于外部（x）[Vytiniotis等，2011]，我们提出了一个排名1的合格变体的推论系统，该变量呈现主要类型。在这种新环境中的技术挑战是处理由Naive合格的打字推断出的模棱两可的类型。我们通过消除量词来解决这个歧义问题，并通过示例证明了该方法的有效性。
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.
登录
查看更多内容
影响因子：
1
作者：
Igarashi, A;Kobayashi, N
通讯作者：
Kobayashi, N
影响因子：
0.5
作者：
Selinger, Peter;Valiron, Benoit
通讯作者：
Valiron, Benoit
DOI：
10.1145/1108970.1108974
发表时间：
2005-11-01
影响因子：
1.3
作者：
Stuckey, PJ;Sulzmann, M
通讯作者：
Sulzmann, M
DOI：
10.4204/eptcs.176.4
发表时间：
2015-01-01
影响因子：
--
作者：
Gan, Edward;Tov, Jesse A.;Morrisett, Greg
通讯作者：
Morrisett, Greg
影响因子：
22.7
作者：
DAVIS, M;LOGEMANN, G;LOVELAND, D
通讯作者：
LOVELAND, D