Type Classes for Lightweight Substructural Types
Type Classes for Lightweight Substructural Types
复制标题
DOI：
10.4204/eptcs.176.4
复制
发表时间：
2015-01-01
影响因子：
--
通讯作者：
Morrisett, Greg
中科院分区：
文献类型：
--
作者：
Gan, Edward;Tov, Jesse A.;Morrisett, Greg
d线性和亚条件类型是强大的工具，但是将它们添加到标准功能编程语言中通常意味着引入额外的注释和打字机械。我们提出了一种轻巧的亚结构类型系统设计，该设计将削弱和收缩为类型类别的结构规则重述；我们用原型语言夹演示了这种设计。夹具支持多态性亚结构类型以及可变参考的表达性系统。同时，它为富含类型类的标准Damas-Hindley-Milner类型系统增加了几乎没有额外的开销。我们已经为核心模型建立了类型的安全性，并在Haskell中实现了具有类型推理的类型检查器。
d Linear and substructural types are powerful tools, but adding them to standard functional programming languages often means introducing extra annotations and typing machinery. We propose a lightweight substructural type system design that recasts the structural rules of weakening and contraction as type classes; we demonstrate this design in a prototype language,Clamp. Clamp supports polymorphic substructural types as well as an expressive system of mutable references. At the same time, it adds little additional overhead to a standard Damas-Hindley-Milner type system enriched with type classes. We have established type safety for the core model and implemented a type checker with type inference in Haskell.