Guarded recursive datatype constructors
Guarded recursive datatype constructors
复制标题
受保护的递归数据类型构造函数
DOI：
10.1145/604131.604150
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Gang Chen
中科院分区：
文献类型：
--
作者：
H. Xi;Chiyan Chen;Gang Chen
我们引入了保护递归（g.r.）的概念。数据类型构造函数，在函数式编程语言（如ML和Haskell）中推广了递归数据库的概念。我们解决的理论和实践问题，由此产生的一般化。一方面，我们设计了一个类型系统来形式化g.r.的概念。数据类型构造函数，然后证明类型系统的可靠性。另一方面，我们提出了一些重要的应用（例如，实现对象，实现阶段计算等）关于G.R.数据类型构造函数，认为g. r.数据类型构造函数可以在编程中产生深远的影响。本文的主要贡献在于认识，然后正式的编程概念，这是理论上的兴趣和实际用途。
We introduce a notion of guarded recursive (g.r.) datatype constructors, generalizing the notion of recursive datatypes in functional programming languages such as ML and Haskell. We address both theoretical and practical issues resulted from this generalization. On one hand, we design a type system to formalize the notion of g.r. datatype constructors and then prove the soundness of the type system. On the other hand, we present some significant applications (e.g., implementing objects, implementing staged computation, etc.) of g.r. datatype constructors, arguing that g.r. datatype constructors can have far-reaching consequences in programming. The main contribution of the paper lies in the recognition and then the formalization of a programming notion that is of both theoretical interest and practical use.