Abstract
We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abbott, M.: Category of Containers. Ph.D. thesis, University of Leicester (2003)
Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theoretical Computer Science 333(1-2), 3–66 (2005)
Aczel, P.: Frege structures and the notions of proposition, truth and set. In: Barwise, J., Keisler, H.J., Kunen, K. (eds.) The Kleene Symposium. Studies in Logic and the Foundations of Mathematics, vol. 101, pp. 31–59. Elsevier (1980)
Adámek, J., Milius, S., Moss, L.: Initial algebras and terminal coalgebras: A survey (June 29, 2010), draft
Blampied, P.: Structured Recursion for Non-uniform Data-types. Ph.D. thesis, University of Nottingham (2000)
Carboni, A., Johnstone, P.: Connected limits, familial representability and Artin glueing. Mathematical Structures in Computer Science 5(4), 441–459 (1995)
Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic 65(2), 525–549 (2000)
Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)
Dybjer, P., Setzer, A.: Induction–recursion and initial algebras. Annals of Pure and Applied Logic 124(1-3), 1–47 (2003)
Dybjer, P., Setzer, A.: Indexed induction–recursion. Journal of Logic and Algebraic Programming 66(1), 1–49 (2006)
Ek, L., Holmström, O., Andjelkovic, S.: Formalizing Arne Andersson trees and Left-leaning Red-Black trees in Agda. Bachelor thesis, Chalmers University of Technology (2009)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. Logic in Computer Science, pp. 193–202 (1999)
Ghani, N., Hamana, M., Uustalu, T., Vene, V.: Representing cyclic structures as nested types (2006), presented at Trends in Functional Programming
Hancock, P., McBride, C., Ghani, N., Malatesta, L., Altenkirch, T.: Small induction recursion. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 156–172. Springer, Heidelberg (2013)
Ghani, N., Malatesta, L., Nordvall Forsberg, F., Setzer, A.: Fibred data types. In: LICS 2013 (2013)
Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Elsevier (1999)
Mark, W.: Familial 2-functors and parametric right adjoints. Theory and Applications of Category Theory 18(22), 665–732 (2007)
Martin-Löf, P.: An intuitionistic theory of types (1972), published in Twenty-Five Years of Constructive Type Theory
Martin-Löf, P.: Intuitionistic type theory. Bibliopolis Naples (1984)
McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004)
Nordvall Forsberg, F., Setzer, A.: A finite axiomatisation of inductive-inductive definitions. In: Berger, U., Hannes, D., Schuster, P., Seisenberger, M. (eds.) Logic, Construction, Computation, Ontos Mathematical Logic, vol. 3, pp. 259–287. Ontos Verlag (2012)
Ralf, H.: Functional pearl: Perfect trees and bit-reversal permutation. Journal of Functional Programming 10(3), 305–317 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghani, N., Malatesta, L., Nordvall Forsberg, F. (2013). Positive Inductive-Recursive Definitions. In: Heckel, R., Milius, S. (eds) Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40206-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-40206-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40205-0
Online ISBN: 978-3-642-40206-7
eBook Packages: Computer ScienceComputer Science (R0)