Guarded recursive datatype constructors

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Lennart Augustsson, Implementing Haskell overloading, Proceedings of the conference on Functional programming languages and computer architecture, p.65-73, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165191]
	2	Kim B. Bruce, Foundations of object-oriented languages: types and semantics, MIT Press, Cambridge, MA, 2002
	3	C. Chen and H. Xi. Implementing typed meta-programming. Available at http://www.cs.bu.edu/char126hwxi/academic/papers/TMP.ps, November 2002.
	4	A. Church. A formulation of the simple type theory of types. Journal of Symbolic Logic, 5:56--68, 1940.
	5	Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
	6	Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
	7	Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Journal of the ACM (JACM), v.48 n.3, p.555-604, May 2001 [doi>10.1145/382780.382785]
	8	Catherine Dubois , François Rouaix , Pierre Weis, Extensional polymorphism, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.118-129, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199473]
	9	Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
	10	Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
	11	Konstantin Läfer , Martin Odersky, Polymorphic type inference and abstract data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1411-1430, Sept. 1994 [doi>10.1145/186025.186031]
	12	Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
	13	Chamond Liu, Smalltalk, objects, and design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
	14	Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
	15	M. Neubauer, P. Thiemann, M. Gasbichler, and M. Sperber. A Functional Notation for Functional Dependencies. In Proceedings of 2001 Haskell Workshop, pages 101--120, Florence, Italy, September 2001.
	16	Atsushi Ohori , Kazuhiko Kato, Semantics for communication primitives in a polymorphic language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.99-112, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158529]
	17	S. Peyton Jones et al. Haskell~98 -- A non-strict, purely functional language. Available at http://www.haskell.org/onlinereport/, Feb. 1999.
	18	F. Pfenning. Computation and Deduction. Cambridge University Press, 2002.
	19	Walid Taha , Tim Sheard, MetaML and multi-stage programming with explicit annotations, Theoretical Computer Science, v.248 n.1-2, p.211-242, October 2000 [doi>10.1016/S0304-3975(00)00053-0]
	20	Andrew Tolmach, Tag-free garbage collection using explicit type parameters, Proceedings of the 1994 ACM conference on LISP and functional programming, p.1-11, June 27-29, 1994, Orlando, Florida, United States
	21	Valery Trifonov , Bratin Saha , Zhong Shao, Fully reflexive intensional type analysis, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.82-93, September 2000
	22	Stephanie Weirich, Encoding Intensional Type Analysis, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.92-106, April 02-06, 2001
	23	Hongwei Xi , Frank Pfenning, Dependent types in practical programming, 1998
	24	H. Xi, C. Chen, and G. Chen. Guarded Recursive Datatype Constructors, 2002. Available at http://www.cs.bu.edu/char126hwxi/GRecTypecon/.
	25	Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]