Hongwei Xi
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.
- L. Augustsson. Implementing Haskell overloading. In Functional Programming Languages and Computer Architecture, 93.]] Google Scholar
Digital Library
- K. B. Bruce. Foundations of Object-Oriented Languages. The MIT Press, Cambridge, MA, 2002.]] Google ScholarDigital Library
- C. Chen and H. Xi. Implementing typed meta-programming. Available at http://www.cs.bu.edu/char126hwxi/academic/papers/TMP.ps, November 2002.]]Google Scholar
- A. Church. A formulation of the simple type theory of types. Journal of Symbolic Logic, 5:56--68, 1940.]]Google ScholarCross Ref
- K. Crary and S. Weirich. Flexible Type Analysis. In Proceedings of International Conference on Functional Programming (ICFP '99), Paris, France, 1999.]] Google ScholarDigital Library
- K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proceedings of the International Conference on Functional Programming (ICFP '98), pages 301--312, Baltimore, MD, September 1998.]] Google ScholarDigital Library
- R. Davies and F. Pfenning. A Modal Analysis of Staged Computation. Journal of ACM, 2002.]] Google ScholarDigital Library
- C. Dubois, F. Rouaix, and P. Weis. Generic Polymorphism. In Proceeding of the 22th ACM Symposium on Principles of Programming Languages (POPL '95), pages 118--129, London, UK, January 1995.]] Google ScholarDigital Library
- A. Goldenberg and D. Robson. Smalltalk-80: The Language and Its Implementation. Addison Wesley, 1983.]] Google ScholarDigital Library
- R. W. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Conference Record of POPL '95: 22nd ACM SIGPLAN Symposium on Principles of Programming Languages, pages 130--141, San Francisco, 1995.]] Google ScholarDigital Library
- K. Läufer and M. Odersky. Ploymorphic Type Inference and Abstract Data Types. ACM Transactions of Programming Languages and Systems (TOPLAS), 16(5):1411--1430, September 1994.]] Google ScholarDigital Library
- X. Leroy. Unboxed objects and polymorphic typing. In Conference Record of the Nineteenth Annual ACM SIGPLAN Symposium on Principles of Programming Languages, pages 177--188, Albuquerque, New Mexico, January 1992.]] Google ScholarDigital Library
- C. Liu. Smalltalk, Objects, and Design. Manning Publications Co., Greenwich, CT 06830, 1996.]] Google ScholarDigital Library
- R. Milner, M. Tofte, R. W. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts, 1997.]] Google ScholarDigital Library
- 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.]]Google Scholar
- A. Ohori and K. Kato. Semantics for communication primitives in a polymorphic language. In Conference Record of the Twentieth Annual ACM SIGPLAN Symposium on Principles of Programming Languages, pages 99--112, Charleston, SC, January 1993.]] Google ScholarDigital Library
- S. Peyton Jones et al. Haskell~98 -- A non-strict, purely functional language. Available at http://www.haskell.org/onlinereport/, Feb. 1999.]]Google Scholar
- F. Pfenning. Computation and Deduction. Cambridge University Press, 2002.]]Google Scholar
- W. Taha and T. Sheard. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1-2):211--242, 2000.]] Google ScholarDigital Library
- A. Tolmach. Tag-free garbage collection using explicit type parameters. In Proceedings of ACM Conference on LISP and Functional Programming, pages 1--11, Orlando, FL, June 1994.]] Google ScholarDigital Library
- V. Trifonov, B. Saha, and Z. Shao. Fully Reflexive Intensional Type Analysis. In Proceedings of the International Conference on Functional Programming, September 1999.]] Google ScholarDigital Library
- S. Weirich. Encoding intensional type analysis. In D. Sands, editor, Programming Languages and Systems: 10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2--6, 2001, volume 2028 of Lecture Notes in Computer Science, pages 92--106. Springer, 2001.]] Google ScholarDigital Library
- H. Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, 1998. pp. viii+189. Available at http://www.cs.cmu.edu/char126hwxi/DML/thesis.ps.]] Google ScholarDigital Library
- H. Xi, C. Chen, and G. Chen. Guarded Recursive Datatype Constructors, 2002. Available at http://www.cs.bu.edu/char126hwxi/GRecTypecon/.]]Google Scholar
- H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pages 214--227, San Antonio, Texas, January 1999.]] Google ScholarDigital Library
Index Terms
- Guarded recursive datatype constructors
Recommendations
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 ...
Self type constructors
OOPSLA '09: Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applicationsBruce and Foster proposed the language LOOJ, an extension of Java with the notion of MyType, which represents the type of a self reference and changes its meaning along with inheritance. MyType is useful to write extensible yet type-safe classes for ...
Self type constructors
OOPSLA '09Bruce and Foster proposed the language LOOJ, an extension of Java with the notion of MyType, which represents the type of a self reference and changes its meaning along with inheritance. MyType is useful to write extensible yet type-safe classes for ...
Comments