Stefan Monnier
ABSTRACT
Algebraic data types and inductive types like those of the Calculus of Inductive Constructions (CIC) are the bread and butter of statically typed functional programming languages. They conveniently combine in a single package product types, sum types, recursive types, and indexed types. But this also makes them somewhat heavyweight: for example, tuples have to be defined as "degenerate" single constructor inductive types, and extraction of a single field becomes a laborious full case-analysis on the object. We consider this to be unsatisfactory. In this article, we develop an alternative presentation of CIC's inductive types where the various elements are provided separately, such that inductive types are built on top of tuples and sums rather than the other way around. The resulting language is lower-level yet we show it can be translated to to a predicative version of the Calculus of Inductive Constructions in a type-preserving way. An additional benefit is that it can conveniently give a precise type to the default branch of "case" statements.
- Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury. 2010. ΠΣ: Dependent Types without the Sugar. In International Symposium on Functional and Logic Programming. 40–55. Google Scholar
Digital Library
- Henk P. Barendregt. 1991. Introduction to generalized type systems. Journal of Functional Programming 1, 2 (April 1991), 121–154.Google ScholarCross Ref
- Bruno Barras and Bruno Bernardo. 2008. Implicit Calculus of Constructions as a Programming Language with Dependent Types. In Conference on Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Vol. 4962. Budapest, Hungary. Google ScholarDigital Library
- Matthias Blume, Umut A. Acar, and Wonseok Chae. 2006. Extensible programming with first-class cases. In International Conference on Functional Programming. Portland, Oregon, 239–250. Google ScholarDigital Library
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.Google ScholarCross Ref
- Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining proofs and programs in a dependently typed language. In Symposium on Principles of Programming Languages. ACM Press, 33–45. Google ScholarDigital Library
- Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyên. 2016. Settheoretic types for polymorphic variants. In International Conference on Functional Programming. 378–391. Google ScholarDigital Library
- James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. 2010. The Gentle Art of Levitation. In International Conference on Functional Programming. Baltimore, MD, 3–14. Google ScholarDigital Library
- Thierry Coquand. 1992. Pattern Matching with Dependent Types. In Workshop on Types for Proofs and Programs. 66–79.Google Scholar
- Denis Firsov and Aaron Stump. 2018. Generic Derivation of Induction for Impredicative Encodings in Cedille. In Certified Programs and Proofs. 215–227. Google ScholarDigital Library
- Eduardo Giménez. 1994. Codifying guarded definitions with recursive schemes. Technical Report RR1995-07. École Normale Supérieure de Lyon.Google Scholar
- Gérard P. Huet, Christine Paulin-Mohring, et al. 2000. The Coq Proof Assistant Reference Manual. Part of the Coq system version 6.3.1.Google Scholar
- Xavier Leroy. 1992. Unboxed Objects and Polymorphic Typing. In Symposium on Principles of Programming Languages. 177–188. Google ScholarDigital Library
- Xavier Leroy. 1997. The Effectiveness of Type-Based Unboxing. In International Workshop on Types in Compilation. BCCS-97-03.Google Scholar
- Zhaohui Luo. 1989. ECC, an Extended Calculus of Constructions. In Annual Symposium on Logic in Computer Science. 386–395. Google ScholarDigital Library
- Robin Milner, Mads Tofte, Robert Harper, and David B. MacQueen. 1997. The Definition of Standard ML Revised. MIT Press, Cambridge, Massachusetts. Google ScholarDigital Library
- Alexandre Miquel. 2001. The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping. In International conference on Typed Lambda Calculi and Applications. 344– 359. Google ScholarDigital Library
- Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Conference on Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Vol. 4962. Budapest, Hungary, 350–364. Google ScholarDigital Library
- Stefan Monnier. 2007. The Swiss Coercion. In Programming Languages meets Program Verification. ACM Press, Freiburg, Germany, 33–40. Google ScholarDigital Library
- Stefan Monnier. 2019. Typer: ML boosted with type theory and Scheme. In Journées Francophones des Langages Applicatifs. 193–208.Google Scholar
- Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. Dissertation. Chalmers university.Google Scholar
- Martin Odersky and Philip Wadler. 1997. Pizza into Java: Translating Theory into Practice. In Symposium on Principles of Programming Languages. Google ScholarDigital Library
- Christine Paulin-Mohring. 1993. Inductive definitions in the system Coq— rules and properties. In International conference on Typed Lambda Calculi and Applications, M. Bezem and J. Groote (Eds.). LNCS 664, SpringerVerlag, 328–345. Google ScholarDigital Library
- Zhong Shao. 1997. Flexible Representation Analysis. In International Conference on Functional Programming. ACM Press, 85–98. Google ScholarDigital Library
- Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007. System F with Type Equality Coercions. In Types in Language Design and Implementation. Nice, France, 53–66. Google ScholarDigital Library
- Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-monadic Effects in F*. In Symposium on Principles of Programming Languages. ACM Press, 256–270. Google ScholarDigital Library
Index Terms
- Inductive types deconstructed: the calculus of united constructions
Recommendations
Type Theory based on Dependent Inductive and Coinductive Types
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceWe develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For ...
Impredicative Encodings of (Higher) Inductive Types
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer SciencePostulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and ...
Mendler-style inductive types, categorically
We 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-...
Comments