AbstractWe present a basis for a category-theoretic account of Mendler-style inductive types. The account is based on suitably defined concepts of Mendler-style algebra and algebra homomorphism; Mendler-style inductive types are identified with initial Mendler-style algebras. We use the identification to obtain a reduction of conventional inductive types to Mendler-style inductive types and a reduction in the presence of certain restricted existential types of Mendler-style inductive types to conventional inductive types.
Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic
Additional Key Words and Phrases: inductive types, initial algebras, prefixed points, Mendler-style, typed functional programming, categorical program calculation
Selected papers that cite this one
- Tarmo Uustalu, Varmo Vene, and Alberto Pardo. Recursion Schemes from Comonads. Nordic Journal of Computing, 8(3):366-390, Fall 2001.
Selected references
- M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theoretical Computer Science, 121(1-2):9-58, 6 December 1993.
- E. S. Bainbridge, P. J. Freyd, A. Scedorov, and P. J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35-64, 15 January 1990.
- Peter Freyd. Recursive types reduced to inductive types. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 498-507, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- P. Freyd. Structural polymorphism. Theoretical Computer Science, 115(1):107-129, 5 July 1993.
- Ryu Hasegawa. Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science, 4(1):71-109, March 1994.
- Daniel J. Lehmann and Michael B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, 14:97-139, 1981.
- Grant Malcolm. Data structures and program transformation. Science of Computer Programming, 14(2-3):255-279, October 1990.
- N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings, Symposium on Logic in Computer Science, pages 30-36, Ithaca, New York, 22-25 June 1987. The Computer Society of the IEEE.
- N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1-2):159-172, 1991.
- M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761-783, November 1982.
- Mitchell Wand. Fixed-point constructions in order-enriched categories. Theoretical Computer Science, 8(1):13-30, February 1979.