research-article

Open access

Normalization by evaluation for sized dependent types

Authors:

Andrea Vezzosi,

Theo WinterhalterAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 1, Issue ICFP

Article No.: 33, Pages 1 - 30

https://doi.org/10.1145/3110277

Published: 29 August 2017 Publication History

Abstract

Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics.

In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier ∀ which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Π for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.

Supplementary Material

Auxiliary Archive (icfp17-main84-s.zip)

Sit = Size-irrelevant types Sit is a prototypical language with an Agda-compatible syntax. It has dependent function types, universes, sized natural numbers, and case and recursion over natural numbers. There is a relevant and an irrelevant quantifier over sizes. For an example, see file test/Test.agda.

Download
42.93 KB

References

[1]

Andreas Abel. 2008. Semi-continuous Sized Types and Termination. Logical Methods in Computer Science 4, 2:3 (2008), 1–33.

[2]

Andreas Abel. 2010. Towards Normalization by Evaluation for the β η-Calculus of Constructions. In Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings (Lecture Notes in Computer Science), Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.), Vol. 6009. Springer, 224–239.

Digital Library

[3]

Andreas Abel. 2012. Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types. In Proceedings of the 8th Workshop on Fixed Points in Computer Science (FICS 2012) (Electronic Proceedings in Theoretical Computer Science), Dale Miller and Zoltán Ésik (Eds.), Vol. 77. 1–11.

[4]

Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Unpublished. http://www.tcs.ifi. lmu.de/~abel/habil.pdf

[5]

Andreas Abel and Thorsten Altenkirch. 2002. A Predicative Analysis of Structural Recursion. Journal of Functional Programming 12, 1 (2002), 1–41.

Digital Library

[6]

Andreas Abel, Thierry Coquand, and Peter Dybjer. 2007. Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings. IEEE Computer Society Press, 3–12.

Digital Library

[7]

Andreas Abel, Thierry Coquand, and Miguel Pagano. 2009. A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. In Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009, Proceedings (Lecture Notes in Computer Science), Pierre-Louis Curien (Ed.), Vol. 5608. Springer, 5–19.

Digital Library

[8]

Andreas Abel, Thierry Coquand, and Miguel Pagano. 2011. A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. Logical Methods in Computer Science 7, 2:4 (2011), 1–57.

[9]

Andreas Abel and Brigitte Pientka. 2016. Well-founded recursion with copatterns and sized types. Journal of Functional Programming 26 (2016), 61.

[10]

Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1:29 (2012), 1–36.

[11]

AgdaTeam. 2017. The Agda Wiki. (2017). http://wiki.portal.chalmers.se/agda

[12]

Roberto M. Amadio (Ed.). 2008. Foundations of Software Science and Computational Structures, 11th International Conference, FoSSaCS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings. Lecture Notes in Computer Science, Vol. 4962. Springer.

[13]

Roberto M. Amadio and Solange Coupet-Grimal. 1998. Analysis of a Guard Condition in Type Theory (Extended Abstract). In Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings (Lecture Notes in Computer Science), Maurice Nivat (Ed.), Vol. 1378. Springer, 48–62.

[14]

Henk Barendregt. 1991. Introduction to Generalized Type Systems. Journal of Functional Programming 1, 2 (1991), 125–154.

[15]

Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types, See [ Amadio 2008 ], 365–379.

[16]

Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto, and Tarmo Uustalu. 2004. Type-Based Termination of Recursive Definitions. Mathematical Structures in Computer Science 14, 1 (2004), 97–141.

Digital Library

[17]

Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski. 2006. CICˆ: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings (Lecture Notes in Computer Science), Miki Hermann and Andrei Voronkov (Eds.), Vol. 4246. Springer, 257–271.

Digital Library

[18]

Gilles Barthe, Benjamin Grégoire, and Colin Riba. 2008a. A Tutorial on Type-Based Termination. In LerNet ALFA Summer School (Lecture Notes in Computer Science), Ana Bove, Luís Soares Barbosa, Alberto Pardo, and Jorge Sousa Pinto (Eds.), Vol. 5520. Springer, 100–152.

Digital Library

[19]

Gilles Barthe, Benjamin Grégoire, and Colin Riba. 2008b. Type-Based Termination with Sized Products. In Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings (Lecture Notes in Computer Science), Michael Kaminski and Simone Martini (Eds.), Vol. 5213. Springer, 493–507.

Digital Library

[20]

Ulrich Berger and Helmut Schwichtenberg. 1991. An Inverse to the Evaluation Functional for Typed λ-calculus. In Sixth Annual Symposium on Logic in Computer Science (LICS ’91), July, 1991, Amsterdam, The Netherlands, Proceedings. IEEE Computer Society Press, 203–211.

[21]

Frédéric Blanqui. 2004. A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems. In Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3 – 5, 2004, Proceedings (Lecture Notes in Computer Science), Vincent van Oostrom (Ed.), Vol. 3091. Springer, 24–39.

[22]

Frédéric Blanqui. 2005. Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. In Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings (Lecture Notes in Computer Science), C.-H. Luke Ong (Ed.), Vol. 3634. Springer, 135–150.

Digital Library

[23]

Frédéric Blanqui and Colin Riba. 2006. Combining Typing and Size Constraints for Checking the Termination of HigherOrder Conditional Rewrite Systems. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings (Lecture Notes in Computer Science), Miki Hermann and Andrei Voronkov (Eds.), Vol. 4246. Springer, 105–119.

Digital Library

[24]

Ana Bove. 2009. Another Look at Function Domains. Electronic Notes in Theoretical Computer Science 249 (2009), 61–74.

Digital Library

[25]

Ana Bove and Venanzio Capretta. 2005. Modelling general recursion in type theory. Mathematical Structures in Computer Science 15, 4 (2005), 671–708.

Digital Library

[26]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.

[27]

Thierry Coquand. 1996. An Algorithm for Type-Checking Dependent Types, In Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction ( July 17–21, 1995, Kloster Irsee, Germany). Science of Computer Programming 26, 1-3, 167–177.

Digital Library

[28]

Olivier Danvy. 1999. Type-Directed Partial Evaluation. In Partial Evaluation – Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998 (Lecture Notes in Computer Science), John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann (Eds.), Vol. 1706. Springer, 367–411.

[29]

N. G. de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34 (1972), 381–392.

[30]

Peter Dybjer. 2000. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. The Journal of Symbolic Logic 65, 2 (2000), 525–549.

[31]

Peter Dybjer, Bengt Nordström, and Jan M. Smith (Eds.). 1995. Types for Proofs and Programs, International Workshop TYPES’94, Båstad, Sweden, June 6-10, 1994, Selected Papers. Lecture Notes in Computer Science, Vol. 996. Springer.

[32]

Daniel Fridlender and Miguel Pagano. 2013. A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation. In Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings (Lecture Notes in Computer Science), Masahito Hasegawa (Ed.), Vol. 7941. Springer, 140–155.

[33]

Herman Geuvers. 1994. A short and flexible proof of Strong Normalization for the Calculus of Constructions, See [ Dybjer et al. 1995 ], 14–38.

[34]

Eduardo Giménez. 1995. Codifying Guarded Definitions with Recursive Schemes, See [ Dybjer et al. 1995 ], 39–59.

[35]

Benjamin Grégoire and Xavier Leroy. 2002. A compiled implementation of strong reduction. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002 (SIGPLAN Notices), Vol. 37. ACM Press, 235–246.

Digital Library

[36]

Benjamin Grégoire and Jorge Luis Sacchini. 2010. On Strong Normalization of the Calculus of Constructions with Type-Based Termination. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings (Lecture Notes in Computer Science), Christian G. Fermüller and Andrei Voronkov (Eds.), Vol. 6397. Springer, 333–347.

[37]

Robert Harper and Frank Pfenning. 2005. On Equivalence and Canonical Forms in the LF Type Theory. ACM Transactions on Computational Logic 6, 1 (2005), 61–101.

Digital Library

[38]

Gérard P. Huet. 1989. The Constructive Engine. In A Perspective in Theoretical Computer Science - Commemorative Volume for Gift Siromoney, R. Narasimhan (Ed.). World Scientific Series in Computer Science, Vol. 16. World Scientific, 38–69.

[39]

John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 410–423.

Digital Library

[40]

INRIA. 2016. The Coq Proof Assistant Reference Manual (version 8.6 ed.). INRIA. http://coq.inria.fr/

[41]

Ugo Dal Lago and Charles Grellois. 2017. Probabilistic Termination by Monadic Affine Sized Typing. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 393–419.

[42]

Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The Size-Change Principle for Program Termination. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, Chris Hankin and Dave Schmidt (Eds.). ACM Press, 81–92.

Digital Library

[43]

William Lovas and Frank Pfenning. 2010. Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance. Logical Methods in Computer Science 6, 4 (2010).

[44]

Per Martin-Löf. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium ‘73, H. E. Rose and J. C. Shepherdson (Eds.). North-Holland, 73–118.

[45]

Alexandre Miquel. 2000. A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping. In 15th Annual IEEE Symposium on Logic in Computer Science (LICS 2000), 26-29 June 2000, Santa Barbara, California, USA, Proceedings. IEEE Computer Society Press, 18–29.

[46]

Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings (Lecture Notes in Computer Science), Samson Abramsky (Ed.), Vol. 2044. Springer, 344–359.

[47]

Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems, See [ Amadio 2008 ], 350–364.

[48]

Bengt Nordström. 1988. Terminating General Recursion. BIT 28, 3 (1988), 605–619.

Digital Library

[49]

Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden.

[50]

Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In 16th IEEE Symposium on Logic in Computer Science (LICS 2001), 16-19 June 2001, Boston University, USA, Proceedings. IEEE Computer Society Press, 221–230.

[51]

Jorge Luis Sacchini. 2013. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. IEEE Computer Society Press, 233–242.

Digital Library

[52]

Jorge Luis Sacchini. 2014. Linear Sized Types in the Calculus of Constructions. In Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings (Lecture Notes in Computer Science), Michael Codish and Eijiro Sumii (Eds.), Vol. 8475. Springer, 169–185.

[53]

Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. 2010. Termination Casts: A Flexible Approach to Termination with General Recursion. In Workshop on Partiality And Recursion in Interactive Theorem Provers, PAR 2010, Satellite Workshop of ITP’10 at FLoC 2010 (Electronic Proceedings in Theoretical Computer Science), Ana Bove, Ekaterina Komendantskaya, and Milad Niqui (Eds.), Vol. 43. 76–93.

[54]

Martin Sulzmann, Manuel M. T. Chakravarty, Simon L. Peyton Jones, and Kevin Donnelly. 2007. System F with type equality coercions. In Proceedings of TLDI’07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007, François Pottier and George C. Necula (Eds.). ACM Press, 53–66.

Digital Library

[55]

David Wahlstedt. 2007. Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion. Ph.D. Dissertation. Chalmers University of Technology.

[56]

Benjamin Werner. 1992. A Normalization Proof for an Impredicative Type System with Large Eliminations over Integers. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, June 1992, Bengt Nordström, Kent Petersson, and Gordon Plotkin (Eds.). 341–357. http://www.cs.chalmers.se/Cs/Research/Logic/Types/proc92.ps

[57]

Hongwei Xi. 2002. Dependent Types for Program Termination Verification. Journal of Higher-Order and Symbolic Computation 15, 1 (2002), 91–131.

Digital Library

Cited By

Winterhalter T(2024)Dependent Ghosts Have a Reflection for FreeProceedings of the ACM on Programming Languages10.1145/36746478:ICFP(630-658)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674647
Felicissimo T(2024)Generic bidirectional typing for dependent type theoriesProgramming Languages and Systems10.1007/978-3-031-57262-3_6(143-170)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57262-3_6
HU JJANG JPIENTKA B(2023)Normalization by evaluation for modal dependent type theoryJournal of Functional Programming10.1017/S095679682300006033Online publication date: 2-Oct-2023
https://doi.org/10.1017/S0956796823000060
Show More Cited By

Index Terms

Normalization by evaluation for sized dependent types
1. Theory of computation
  1. Logic
    1. Type theory
  2. Semantics and reasoning

Recommendations

Definitional Functoriality for Dependent (Sub)Types
Programming Languages and Systems
Abstract
Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws, equations ... $_{}$
Label dependent lambda calculus and gradual typing

Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a ...
Integrating Linear and Dependent Types
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency. Next, we give an application of this calculus by giving a proof-theoretic account of imperative ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 1, Issue ICFP

September 2017

1173 pages

EISSN:2475-1421

DOI:10.1145/3136534

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2017

Published in PACMPL Volume 1, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

33
Total Citations
View Citations
704
Total Downloads

Downloads (Last 12 months)122
Downloads (Last 6 weeks)37

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Winterhalter T(2024)Dependent Ghosts Have a Reflection for FreeProceedings of the ACM on Programming Languages10.1145/36746478:ICFP(630-658)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674647
Felicissimo T(2024)Generic bidirectional typing for dependent type theoriesProgramming Languages and Systems10.1007/978-3-031-57262-3_6(143-170)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57262-3_6
HU JJANG JPIENTKA B(2023)Normalization by evaluation for modal dependent type theoryJournal of Functional Programming10.1017/S095679682300006033Online publication date: 2-Oct-2023
https://doi.org/10.1017/S0956796823000060
Baunsgaard Kristensen MMogelberg RVezzosi A(2022)Greatest HITs: Higher inductive types in coinductive definitions via induction under clocksProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533359(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533359
Wang XHuang RYang CMao S(2021)Smartphone Sonar-Based Contact-Free Respiration Rate MonitoringACM Transactions on Computing for Healthcare10.1145/34368222:2(1-26)Online publication date: 9-Feb-2021
https://dl.acm.org/doi/10.1145/3436822
Sherman BMichel JCarbin M(2021)𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypesProceedings of the ACM on Programming Languages10.1145/34342845:POPL(1-31)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434284
Bahr PGraulund CMøgelberg R(2021)Diamonds are not forever: liveness in reactive programming with guarded recursionProceedings of the ACM on Programming Languages10.1145/34342835:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434283
Weng WZhou XSrikant R(2021)Optimal Load Balancing with Locality ConstraintsProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/34283304:3(1-37)Online publication date: 15-Jun-2021
https://dl.acm.org/doi/10.1145/3428330
Abanto-Leon LBäuml ASim GHollick MAsadi A(2021)Stay Connected, Leave no TraceProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/34283294:3(1-31)Online publication date: 15-Jun-2021
https://dl.acm.org/doi/10.1145/3428329
Ma YZeng YJain V(2020)CarOSenseProceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies10.1145/34118204:3(1-28)Online publication date: 4-Sep-2020
https://dl.acm.org/doi/10.1145/3411820
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents