Variations on Inductive-Recursive Definitions
Dybjer and Setzer introduced the definitional principle of inductive-recursively defined families - i.e. of families (U : Set, T : U -> D) such that the inductive definition of U may depend on the recursively defined T --- by defining a type DS D E of codes. Each c : DS D E defines a functor [c] : Fam D -> Fam E, and
(U, T) = \mu [c] : Fam D is exhibited as the initial algebra of [c].
This paper considers the composition of DS-definable functors: Given F : Fam C -> Fam D and G : Fam D -> Fam E, is G \circ F : Fam C -> Fam E DS-definable, if F and G are? We show that this is the case if and only if powers of families are DS-definable, which seems unlikely. To construct composition, we present two new systems UF and PN of codes for inductive-recursive definitions, with UF a subsytem of DS a subsystem of PN. Both UF and PN are closed under composition. Since PN defines a potentially larger class of functors, we show that there is a model where initial algebras of PN-functors exist by adapting Dybjer-Setzer's proof for DS.
Type Theory
induction-recursion
initial-algebra semantics
63:1-63:13
Regular Paper
Neil
Ghani
Neil Ghani
Conor
McBride
Conor McBride
Fredrik
Nordvall Forsberg
Fredrik Nordvall Forsberg
Stephan
Spahn
Stephan Spahn
10.4230/LIPIcs.MFCS.2017.63
Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. TCS, 342(1):3 - 27, 2005.
Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. Journal Functional Programming, 25, 2015.
James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In ICFP 2010, pages 3-14, 2010.
Peter Dybjer. Inductive families. Formal aspects of computing, 6(4):440-465, 1994.
Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), 2000.
Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In TLCA, pages 129-146. Springer Verlag, 1999.
Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124(1-3):1-47, 2003.
Peter Dybjer and Anton Setzer. Indexed induction-recursion. Journal of logic and algebraic programming, 66(1):1-49, 2006.
Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Types for Proofs and Programs, pages 210-225, 2004.
Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154:153-192, 2013.
Neil Ghani and Peter Hancock. Containers, monads and induction recursion. Mathematical Structures in Computer Science, 26(1):89-113, 2016.
Peter Hancock. Private communication.
Per Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975.
Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984.
Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13(3):386-402, 2002.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode