Guarded recursive datatype constructors
Top Cited Papers
- 15 January 2003
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 38 (1) , 224-235
- https://doi.org/10.1145/604131.604150
Abstract
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.Keywords
This publication has 14 references indexed in Scilit:
- A modal analysis of staged computationJournal of the ACM, 2001
- MetaML and multi-stage programming with explicit annotationsTheoretical Computer Science, 2000
- Fully reflexive intensional type analysisPublished by Association for Computing Machinery (ACM) ,2000
- Flexible type analysisPublished by Association for Computing Machinery (ACM) ,1999
- Intensional polymorphism in type-erasure semanticsPublished by Association for Computing Machinery (ACM) ,1998
- Compiling polymorphism using intensional type analysisPublished by Association for Computing Machinery (ACM) ,1995
- Polymorphic type inference and abstract data typesACM Transactions on Programming Languages and Systems, 1994
- Implementing Haskell overloadingPublished by Association for Computing Machinery (ACM) ,1993
- Semantics for communication primitives in a polymorphic languagePublished by Association for Computing Machinery (ACM) ,1993
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940