Document Open Access Logo

Simulating Large Eliminations in Cedille

Authors Christa Jenkins , Andrew Marmaduke, Aaron Stump

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.9.pdf
  • Filesize: 0.81 MB
  • 22 pages

Document Identifiers

Author Details

Christa Jenkins
  • The University of Iowa, Iowa City, IA, USA
Andrew Marmaduke
  • The University of Iowa, Iowa City, IA, USA
Aaron Stump
  • The University of Iowa, Iowa City, IA, USA

Cite AsGet BibTex

Christa Jenkins, Andrew Marmaduke, and Aaron Stump. Simulating Large Eliminations in Cedille. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.9

Abstract

Large eliminations provide an expressive mechanism for arity- and type-generic programming. However, as large eliminations are closely tied to a type theory’s primitive notion of inductive type, this expressivity is not expected within polymorphic lambda calculi in which datatypes are encoded using impredicative quantification. We report progress on simulating large eliminations for datatype encodings in one such type theory, the calculus of dependent lambda eliminations (CDLE). Specifically, we show that the expected computation rules for large eliminations, expressed using a derived type of extensional equality of types, can be proven within CDLE. We present several case studies, demonstrating the adequacy of this simulation for a variety of generic programming tasks, and a generic formulation of the simulation allowing its use for a broad family of datatype encodings. All results have been mechanically checked by Cedille, an implementation of CDLE.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • large eliminations
  • generic programming
  • impredicative encodings
  • Cedille
  • Mendler algebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and E. Moran. Innovations in computational type theory using NuPRL. J. Applied Logic, 4(4):428-469, 2006. URL: https://doi.org/10.1016/j.jal.2005.10.005.
  2. Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 56-65. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  3. Gilles Barthe and Maria João Frade. Constructor subtyping. In S. Doaitse Swierstra, editor, Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, 22-28 March, 1999, Proceedings, volume 1576 of Lecture Notes in Computer Science, pages 109-127. Springer, 1999. URL: https://doi.org/10.1007/3-540-49099-X_8.
  4. Corrado Böhm, Mariangiola Dezani-Ciancaglini, P. Peretti, and Simona Ronchi Della Rocca. A discrimination algorithm inside lambda-beta-calculus. Theor. Comput. Sci., 8:265-292, 1979. URL: https://doi.org/10.1016/0304-3975(79)90014-8.
  5. R. M. Burstall and J. A. Goguen. Algebras, Theories and Freeness: An Introduction for Computer Scientists, pages 329-349. Springer Netherlands, Dordrecht, 1982. URL: https://doi.org/10.1007/978-94-009-7893-5_11.
  6. James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 3-14, 2010. URL: https://doi.org/10.1145/1863543.1863547.
  7. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science, pages 50-66. Springer, 1988. URL: https://doi.org/10.1007/3-540-52335-9_47.
  8. Pierre-Évariste Dagand. A cosmology of datatypes: reusability and dependent types. PhD thesis, University of Strathclyde, Glasgow, UK, 2013. URL: http://oleg.lib.strath.ac.uk/R/?func=dbin-jump-full&object_id=22713.
  9. Pierre-Évariste Dagand and Conor McBride. Elaborating inductive definitions. CoRR, abs/1210.6390, 2012. URL: http://arxiv.org/abs/1210.6390.
  10. Cedille development team. Cedille v1.2.1. URL: https://github.com/cedille/cedille.
  11. Larry Diehl, Denis Firsov, and Aaron Stump. Generic zero-cost reuse for dependent types. Proc. ACM Program. Lang., 2(ICFP):104:1-104:30, July 2018. URL: https://doi.org/10.1145/3236799.
  12. Denis Firsov, Richard Blair, and Aaron Stump. Efficient Mendler-style lambda-encodings in Cedille. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 235-252, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-94821-8_14.
  13. Denis Firsov and Aaron Stump. Generic derivation of induction for impredicative encodings in Cedille. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 215-227, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167087.
  14. Herman Geuvers. Induction is not derivable in second order dependent type theory. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings, volume 2044 of Lecture Notes in Computer Science, pages 166-181, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-45413-6_16.
  15. Tatsuya Hagino. A categorical programming language. PhD thesis, The University of Edinburgh, UK, 1987. Google Scholar
  16. Christopher Jenkins, Colin McDonald, and Aaron Stump. Elaborating inductive definitions and course-of-values induction in Cedille, 2019. URL: http://arxiv.org/abs/1903.08233.
  17. Christopher Jenkins and Aaron Stump. Monotone recursive types and recursive data representations in Cedille. Math. Struct. Comput. Sci., 31(6):682-745, 2021. URL: https://doi.org/10.1017/S0960129521000402.
  18. Patricia Johann, Enrico Ghiorzi, and Daniel Jeffries. GADTs, functoriality, parametricity: Pick two. CoRR, 2021. http://arxiv.org/abs/2105.03389, URL: https://doi.org/10.4204/EPTCS.357.6.
  19. Patricia Johann and Andrew Polonsky. Higher-kinded data types: Syntax and semantics. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785657.
  20. Alexei Kopylov. Dependent intersection: A new way of defining records in type theory. In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, LICS '03, pages 86-95. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210048.
  21. Zhaohui Luo. Coercive subtyping. J. Logic and Computation, 9(1):105-130, 1999. URL: https://doi.org/10.1093/logcom/9.1.105.
  22. Andrew Marmaduke, Christopher Jenkins, and Aaron Stump. Zero-cost constructor subtyping. In IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages, IFL 2020, pages 93-103, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3462172.3462194.
  23. N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Symposium on Logic in Computer Science, (LICS '87), pages 30-36, Los Alamitos, CA, June 1987. IEEE Computer Society. Google Scholar
  24. Alexandre Miquel. The implicit calculus of constructions: Extending pure type systems with an intersection type binder and subtyping. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, TLCA’01, pages 344-359, Berlin, Heidelberg, 2001. Springer-Verlag. URL: https://doi.org/10.1007/3-540-45413-6_27.
  25. Jan M. Smith. An interpretation of Martin-Löf’s type theory in a type-free theory of propositions. J. Symb. Log., 49(3):730-753, 1984. URL: https://doi.org/10.2307/2274128.
  26. Jan M. Smith. The independence of Peano’s fourth axiom from Martin-Lof’s type theory without universes. J. Symb. Log., 53(3):840-845, 1988. URL: https://doi.org/10.2307/2274575.
  27. Aaron Stump. The calculus of dependent lambda eliminations. J. Funct. Program., 27:e14, 2017. URL: https://doi.org/10.1017/S0956796817000053.
  28. Aaron Stump and Christopher Jenkins. Syntax and semantics of Cedille, 2018. URL: http://arxiv.org/abs/1806.04709.
  29. Martin Sulzmann, Manuel M. T. Chakravarty, Simon L. Peyton Jones, and Kevin Donnelly. System F with type equality coercions. In François Pottier and George C. Necula, editors, Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007, pages 53-66. ACM, 2007. URL: https://doi.org/10.1145/1190315.1190324.
  30. Nikhil Swamy, Michael W. Hicks, and Gavin M. Bierman. A theory of typed coercions and its applications. In Graham Hutton and Andrew P. Tolmach, editors, Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, pages 329-340. ACM, 2009. URL: https://doi.org/10.1145/1596550.1596598.
  31. The Coq Development Team. The Coq Reference Manual, version 8.13, 2021. Available electronically at URL: https://coq.github.io/doc/v8.13/refman/.
  32. Tarmo Uustalu and Varmo Vene. Mendler-style inductive types, categorically. Nordic Journal of Computing, 6(3):343-361, September 1999. URL: http://dl.acm.org/citation.cfm?id=774455.774462.
  33. Tarmo Uustalu and Varmo Vene. Coding recursion a la Mendler (extended abstract). In Proc. of the 2nd Workshop on Generic Programming, WGP 2000, Technical Report UU-CS-2000-19, pages 69-85. Dept. of Computer Science, Utrecht University, 2000. Google Scholar
  34. Stephanie Weirich and Chris Casinghino. Generic programming with dependent types. In Jeremy Gibbons, editor, Generic and Indexed Programming - International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures, volume 7470 of Lecture Notes in Computer Science, pages 217-258. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-32202-0_5.
  35. Benjamin Werner. A normalization proof for an impredicative type system with large elimination over integers. In Bengt Nordström, Kent Petersson, and Gordon Plotkin, editors, Proc. of the 1992 Workshop on Types for Proofs and Programs, pages 341-357, June 1992. Google Scholar
  36. Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Alex Aiken and Greg Morrisett, editors, Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, pages 224-235. ACM, 2003. URL: https://doi.org/10.1145/604131.604150.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact