Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-09T20:29:25.322Z Has data issue: false hasContentIssue false
  • English
  • Français

The calculus of dependent lambda eliminations*

Part of: JFP Research Articles

Published online by Cambridge University Press:  09 May 2017

AARON STUMP
AARON STUMP*
Affiliation:
Computer Science, The University of Iowa, Iowa City, IA, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Modern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.

Type
Articles
Information
Journal of Functional Programming , Volume 27 , 2017 , e14
Copyright
Copyright © Cambridge University Press 2017 

Footnotes

*

I gratefully acknowledge NSF support of this project under award 1524519, and DoD support under award FA9550-16-1-0082 (MURI program).

References

Abel, A. & Matthes, R. (2004) Fixed points of type constructors and primitive recursion. In Proceedings of 18th International Workshop Computer Science Logic (CSL), Marcinkowski, Jerzy, & Tarlecki, Andrzej (eds), Lecture Notes in Computer Science, vol. 3210. Springer, pp. 190–204.Google Scholar
Altenkirch, T., Danielsson, N. A., Löh, A. & Oury, N. (2010) PiSigma: Dependent types without the sugar. In Proceedings of 10th International Symposium (Flops) Functional and Logic Programming, Blume, M., Kobayashi, N. & Vidal, G. (eds), Lecture Notes in Computer Science, vol. 6009. Springer, Berlin, Heidelberg, pp. 40–55.CrossRefGoogle Scholar
Atkey, R., Ghani, N. & Johann, P. (2014) A relationally parametric model of dependent type theory. Sigplan Not. 49 (1), 503–515.CrossRefGoogle Scholar
Augustsson, L. (1998) Cayenne – a language with dependent types. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP), Felleisen, M., Hudak, P., & Queinnec, C. (eds). ACM, pp. 239–250.Google Scholar
Berger, U. & Schwichtenberg, H. (1991) An inverse of the evaluation functional for typed lambda-calculus. In Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society, pp. 203–211.CrossRefGoogle Scholar
Bernardy, J.-P. & Lasson, M. (2011) Realizability and parametricity in pure type systems. In Proceedings of 14th International Conference Foundations of Software Science and Computational Structures, Lecture Notes in Computer Science, vol. 6604. Springer, Berlin, Heidelberg, pp. 108–122.Google Scholar
Böhm, C. & Berarducci, A. (1985) Automatic synthesis of typed lambda-programs on term algebras. Theor. Comput. Sci. 39, 135–154.CrossRefGoogle Scholar
Carette, J., Kiselyov, O. & Shan, C.-C. (2009) Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. J. Funct. Program. 19 (5), 509–543.CrossRefGoogle Scholar
Chapman, J., Dagand, P.-É., McBride, C. & Morris, P. (2010) The gentle art of levitation. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), Hudak, P. & Weirich, S. (eds), pp. 3–14. ACM.CrossRefGoogle Scholar
Chlipala, A. (2008) Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), Hook, J. & Thiemann, P. (eds), pp. 143–156. ACM.CrossRefGoogle Scholar
Church, A. (1940) A formulation of the simple theory of types. J. Symb. Log. 5 (2), 56–68.CrossRefGoogle Scholar
Church, A. (1941) The Calculi of Lambda Conversion, Annals of Mathematics Studies, vol. 6. Princeton University Press.Google Scholar
Constable, R. L., Allen, S. F., Bromley, M., Cleaveland, R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T. & Smith, S. F. (1986) Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall.Google Scholar
Coquand, T. (1986) An analysis of Girard's paradox. In Proceedings, Symposium on Logic in Computer Science (LICS), IEEE Computer Society, pp. 227–236.Google Scholar
Coquand, T. (1992) Pattern matching with dependent types. Electronic Proceedings of the 3rd Annual Bra workshop on Logical Frameworks, Nordström, B., Petersson, K. & Plotkin, G. (eds). Available from Coquand's home page.Google Scholar
Coquand, T. & Paulin, C. (1988) Inductively defined types. In Colog-88, International Conference on Computer Logic, Martin-Löf, P. & Mints, G. (eds), Lecture Notes in Computer Science, vol. 417. Springer, pp. 50–66.Google Scholar
Crary, K. (2010) Higher-order representation of substructural logics. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), Hudak, P. & Weirich, S. (eds). ACM, pp. 131–142.CrossRefGoogle Scholar
Fegaras, L. & Sheard, T. (1996) Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In Proceedings of 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Boehm, H.-J. & Steele, G. L. Jr. (eds). ACM, pp. 284–294.Google Scholar
Fortune, S., Leivant, D. & O'Donnell, M. (1983) The expressiveness of simple and second-order type structures. J. ACM 30 (1), 151–185.CrossRefGoogle Scholar
Fu, P. & Stump, A. (2014) Self types for dependently typed lambda encodings. In Proceedings of 25th International Conference on Rewriting Techniques and Applications (RTA) joint with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA), Dowek, G. (ed), Lecture Notes in Computer Science, vol. 8560. Springer, pp. 224–239.Google Scholar
Geuvers, H. (2001) Induction is not derivable in second order dependent type theory. In Typed Lambda Calculi and Applications (TLCA), Abramsky, S. (ed), Lecture Notes in Computer Science, vol 2044. Springer, pp. 166–181.CrossRefGoogle Scholar
Ghani, N., Johann, P. & Fumex, C. (2010) Fibrational induction rules for initial algebras. In Computer Science Logic, 24th International Workshop (CSL), Dawar, A. & Veith, H. (eds), Lecture Notes in Computer Science, vol. 6247. Springer, pp. 336–350.Google Scholar
Girard, J.-Y., Taylor, P. & Lafont, Y. (1989) Proofs and Types. New York, USA: Cambridge University Press.Google Scholar
Goguen, H., McBride, C. & McKinna, J. (2006) Eliminating dependent pattern matching. In Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday, Futatsugi, K., Jouannaud, J.-P. & Meseguer, J. (eds), pp. 521–540.CrossRefGoogle Scholar
Harper, R. & Pollack, R. (1989) Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions (draft). In Tapsoft'89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13–17, 1989, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages (CCIPL), Díaz, J. & Orejas, F. (eds), Lecture Notes in Computer Science, vol. 352. Springer, pp. 241–256.Google Scholar
Hofmann, M. (2000) Safe recursion with higher types and bck-algebra. Ann. Pure Appl. Log. 104 (1–3), 113–166.CrossRefGoogle Scholar
Hofmann, M. & Streicher, T. (1998) The groupoid interpretation of type theory. In Twenty-Five Years of Constructive Type Theory. Oxford Logic Guides, vol. 36. Oxford University Press, pp. 83–111.Google Scholar
Koopman, P., Plasmeijer, R. & Jansen, J. M. (2014) Church encoding of data types considered harmful for implementations. In Proceedings of 26th Symposium on Implementation and Application of Functional Languages (IFL), Plasmeijer, R. & Tobin-Hochstadt, S. (eds). ACM, pp. 4:1–4:12.Google Scholar
Kopylov, A. (2003) Dependent intersection: A new way of defining records in type theory. In Proceedings of 18th IEEE Symp. Log. Comput. Sci. (LICS), pp. 86–95.CrossRefGoogle Scholar
Krishnaswami, N. R. & Dreyer, D. (2013) Internalizing relational parametricity in the extensional calculus of constructions. In Computer Science Logic 2013 (CSL), Rocca, S. R. D. (ed), LIPIcs, vol. 23. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp. 432–451.Google Scholar
Leivant, D. (1983) Reasoning about functional programs and complexity classes associated with type disciplines. In Proceedings of 24th Annual Symposium on Foundations of Computer Science, 1983. IEEE Computer Society, pp. 460–469.Google Scholar
Leivant, D. (1991) Finitely stratified polymorphism. Inf. Comput. 93 (1), 93–113.CrossRefGoogle Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory. Napoli: Bibliopolis.Google Scholar
Mendler, N. (1988) Inductive Definition in Type Theory. PhD Thesis, Cornell University.Google Scholar
Meyer, A. R. & Reinhold, M. B. (1986) “Type” is not a type. In Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). New York, USA: ACM, pp. 287–295.Google Scholar
Miquel, A. (2001) The implicit calculus of constructions extending pure type systems with an intersection type binder and subtyping. In Typed Lambda Calculi and Applications, Abramsky, S. (ed), Lecture Notes in Computer Science, vol. 2044. Springer, pp. 344–359.CrossRefGoogle Scholar
Mogensen, T. Æ. (1992) Efficient self-interpretations in lambda calculus. J. Funct. Program. 2 (3), 345–363.CrossRefGoogle Scholar
Norell, U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden.Google Scholar
Parigot, M. (1988) Programming with proofs: A second order type theory. In European Symposium On Programming (ESOP), Ganzinger, H. (ed), Lecture Notes in Computer Science, vol. 300. Springer, pp. 145–159.Google Scholar
Parigot, M. (1989) On the representation of data in lambda-calculus. In Computer Science Logic (CSL), Börger, E., Büning, HansKleine & Richter, M. (eds), Lecture Notes in Computer Science, vol. 440. Springer, pp. 309–321.Google Scholar
Pfenning, F. & Elliott, C. (1988) Higher-order abstract syntax. Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), Wexelblat, R. L. (ed). ACM, pp. 199–208.Google Scholar
Pfenning, F. & Paulin-Mohring, C. (1989) Inductively defined types in the calculus of constructions. InProceedings of 5th International Conference Mathematical Foundations of Programming Semantics, Main, M. G., Melton, A., Mislove, M. W., & Schmidt, D. A. (eds), Lecture Notes in Computer Science, vol 442. Springer, pp. 209–228.Google Scholar
Pfenning, F. & Schürmann, C. (1999) System description: Twelf - a meta-logical framework for deductive systems. In Proceedings of 16th International Conference on Automated Deduction Automated Deduction - Cade-16, Ganzinger, H. (ed), Lecture Notes in Computer Science, vol. 1632. Springer, pp. 202–206.CrossRefGoogle Scholar
Pientka, B. (2008) A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. InProceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Necula, G. C. & Wadler, P. (eds). ACM, pp. 371–382.Google Scholar
Pierce, B. C. & Turner, D. N. (2000) Local type inference. ACM Trans. Program. Lang. Syst. 22 (1), 1–44.CrossRefGoogle Scholar
Polakow, J. (2015) Embedding a full linear lambda calculus in Haskell. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, pp. 177–188. ACM.CrossRefGoogle Scholar
Poswolsky, A & Schürmann, C. (2009) System description: Delphin – a functional programming language for deductive systems. Electr. Notes Theor. Comput. Sci. 228, 113–120.CrossRefGoogle Scholar
Schürmann, C., Despeyroux, J. & Pfenning, F. (2001) Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266 (1–2), 1–57.CrossRefGoogle Scholar
Stump, A. (2016) Verified Functional Programming in Agda. ACM Books.CrossRefGoogle Scholar
Stump, A. & Fu, P. (2016) Efficiency of lambda-encodings in total type theory. J. Funct. Program. 26 (003).CrossRefGoogle Scholar
Tannen, V. & Coquand, T. (1988) Extensional models for polymorphism. Theor. Comput. Sci. 59, 85–114.CrossRefGoogle Scholar
The Coq development team (2015) The Coq Proof Assistant Reference Manual. LogiCal Project. Version 8.4.Google Scholar
Univalent Foundations Program (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book. Last accessed April 21, 2017.Google Scholar
Washburn, G. & Weirich, S. (2003) Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, pp. 249–262.Google Scholar
Werner, B. (1992) A normalization proof for an impredicative type system with large elimination over integers. In Proceedings of the 1992 Workshop on Types for Proofs and Programs. Available from http://www.cse.chalmers.se/research/group/logic/Types/previousevents.html, last access April 23, 2017. pp. 341–357.Google Scholar
Werner, B. (1994) Une Théorie des Constructions Inductives. PhD Thesis. Paris VII: Université Paris-Diderot.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.