Inductive, coinductive, and pointed types

ABSTRACT

An extension of the simply-typed lambda calculus is presented which contains both well-structured inductive and coinductive types, and which also identifies a class of types for which general recursion is possible. The motivations for this work are certain natural constructions in category theory, in particular the notion of an algebraically bounded functor, due to Freyd. We propose that this is a particularly elegant core language in which to work with recursive objects, since the potential for general recursion is contained in a single operator which interacts well with the facilities for bounded iteration and coiteration.

REFERENCES

• Bar92: Michael Barr. Algebraically compact functors. Journal of Pure and Applied Algebra, 82:211-231, 1992.
• BFPS81: Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof- Theoretical Studies. Number 897 in Lecture Notes in Mathematics. Springer-Verlag, 1981.
• CF92: R. Cockett and T. Fukushima. About CHAR- ITY. Technical Report 92/480/18, University of Calgary, June 1992.
• CP92: Roy L. Crole , Andrew M. Pitts, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Information and Computation, v.98 n.2, p.171-210, June 1992 [doi>10.1016/0890-5401(92)90018-B]
• Fio94: Marcello P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994.
• FM91: Maarten M. Fokkinga and Erik Meijer. Program calculation properties of continuous algebras. Technical Report CS-R9104, CWI, January 1991.
• Fre90: Peter Freyd. Recursive types reduced to inductive types. In Fifth Annual IEEE Symposium on Logic in Computer Science, pages 498-507, 1990.
• Fre91: Peter Freyd. Algebraically comple~e categories. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory: Proceedings, Como 1990, pages 95-104. Springer-Verlag, 1991.
• Fre92: Peter Freyd. Remarks on algebraically compact categories, in M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Applications of Categories in Computer Science, number 177 in London Mathematical Society Lecture Note Series, pages 95-106. Cambridge University Press, 1992. Proceedings of the LMS Symposium, Durham 1991.
• GLT89: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• How92: Brian T. Howard, Fixed points and extensionality in typed functional programming languages, Stanford University, Stanford, CA, 1992
• How93: Brian T. Howard. Inductive, projective, and retractive types. Technical Report MS-CIS-93-14, Department of Computer and Information Science, University of Pennsylvania, 1993.
• How94: Brian T. Howard. The expressive power of inductive and coinductive types. Presented at the Tenth Workshop on the Mathematical Foundations of Programming Semantics, March 1994.
• Kie93: Richard B. Kieburtz. Inductive programming. Technical Report CS/E 93-001, Oregon Graduate Institute of Science and Technology, 1993.
• Klo80: Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, University of Utrecht, 1980. Published as Mathematical Center Tract 129.
• LP95: John Launchbury and Ross Paterson. Parametricity and unboxing with unpointed types. Available at http://www, cse. ogi. edu/~j 1/ Papers/point .ps, 1995.
• LS86: J. Lambek , P. J. Scott, Introduction to higher order categorical logic, Cambridge University Press, New York, NY, 1986
• Mei92: Erik Meijer. Calculating Compilers. PhD thesis, University of Nijmegen, 1992.
• MFP91: Erik Meijer , Maarten Fokkinga , Ross Paterson, Functional programming with bananas, lenses, envelopes and barbed wire, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.124-144, June 1991, Cambridge, Massachusetts, United States
• Mit90: John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• Mog89: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• Mog95: Eugenio Moggi. Metalanguages and applications. Available as ML-notes.4vi.gz by anonymous ftp from theory, doc. i~. ac. uk in directory tfm/papers/MoggiE, October 1995.
• Mul92: Philip S. Mulry. Strong monads, algebras and fixed points. In M.P. Four,nan, P.T. Johnstone, and A.M. Pitts, editor.,;, Applications o/ Categories in Computer Science, number 177 in London Mathematical Society Lecture Note Series, pages 202-216. Cambridge University Press, 1992. Proceedings of the LMS Symposium, Durham 1991.
• Mul93: Philip S. Mulry, Lifting Theorems for Kleisli Categories, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, p.304-319, April 07-10, 1993
• Sim92: Alex K. Simpson. Recursive types in kleisli categories. Available as kleisli,dvi. Z by anonymous ftp from ftp.dcs.ed.ac.uk in directory pub/als, August 1992.
• SP82: Michael B. Smyth and Gordon D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11:761- 783, 1982.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Recursive function theory

General Terms:
Design, Languages, Theory