Guarded recursive datatype constructors

12 years 7 months ago
Guarded recursive datatype constructors
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. Categories and Subject Descriptors D.3.2 [Programming Languages]: Language Classifications--Applicative Languages; D.3.3 [Programming Languages]: Language Constructs and Features-...
Hongwei Xi, Chiyan Chen, Gang Chen
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where POPL
Authors Hongwei Xi, Chiyan Chen, Gang Chen
Comments (0)