A Dependently Typed Language with Dynamic Equality
Pages 44 - 57
Abstract
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.
References
[1]
Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, with and without Types. Proceedings of the ACM on Programming Languages, 1, ICFP (2017), Article 39, Aug., 28 pages. https://doi.org/10.1145/3110283
[2]
Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury. 2010. Π Σ : Dependent Types without the Sugar. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 40–55. isbn:978-3-642-12251-4 https://doi.org/10.1007/978-3-642-12251-4_5
[3]
Lennart Augustsson. 1998. Cayenne a language with dependent types. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98). Association for Computing Machinery, New York, NY, USA. 239–250. isbn:1581130244 https://doi.org/10.1145/289423.289451
[4]
Luca Cardelli. 1986. A Polymorphic [lambda]-calculus with Type: Type. DEC System Research Center, 130 Lytton Avenue, Palo Alto, CA 94301.
[5]
Thierry Coquand. 1996. An algorithm for type-checking dependent types. Science of Computer Programming, 26, 1 (1996), 167–177. issn:0167-6423 https://doi.org/10.1016/0167-6423(95)00021-6
[6]
Thierry Coquand and Makoto Takeyama. 2002. An Implementation of Type:Type. In Types for Proofs and Programs, Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, and Robert Pollack (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 53–62. isbn:978-3-540-45842-5 https://doi.org/10.1007/3-540-45842-5_4
[7]
Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. Comput. Surveys, 54, 5 (2021), Article 98, May, 38 pages. issn:0360-0300 https://doi.org/10.1145/3450952
[8]
Richard A Eisenberg. 2016. Dependent types in haskell: Theory and practice. University of Pennsylvania.
[9]
Joseph Eremondi, Éric Tanter, and Ronald Garcia. 2019. Approximate Normalization for Gradual Dependent Types. Proceedings of the ACM on Programming Languages, 3 (2019), Article 88, July, 30 pages. https://doi.org/10.1145/3341692
[10]
Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02). Association for Computing Machinery, New York, NY, USA. 48–59. isbn:1581134878 https://doi.org/10.1145/581478.581484
[11]
Cormac Flanagan. 2006. Hybrid Type Checking. In ACM Symposium on Principles of Programming Languages (POPL ’06). Association for Computing Machinery, New York, NY, USA. 245–256. isbn:1595930272 https://doi.org/10.1145/1111037.1111059
[12]
Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In ACM Symposium on Principles of Programming Languages (POPL ’16). Association for Computing Machinery, New York, NY, USA. 429–442. isbn:9781450335492 https://doi.org/10.1145/2837614.2837670
[13]
Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, and Stephanie Weirich. 2010. Dependent Types and Program Equivalence. ACM SIGPLAN Notices, 45, 1 (2010), Jan., 275–286. issn:0362-1340 https://doi.org/10.1145/1707801.1706333
[14]
Kenneth Knowles and Cormac Flanagan. 2009. Compositional Reasoning and Decidable Checking for Dependent Contract Types. In Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification (PLPV ’09). Association for Computing Machinery, New York, NY, USA. 27––38. isbn:9781605583303 https://doi.org/10.1145/1481848.1481853
[15]
Kenneth Knowles and Cormac Flanagan. 2010. Hybrid Type Checking. ACM Transactions on Programming Languages and Systems, 32, 2 (2010), Article 6, feb, 34 pages. issn:0164-0925 https://doi.org/10.1145/1667048.1667051
[16]
Nico Lehmann and Éric Tanter. 2017. Gradual Refinement Types. ACM SIGPLAN Notices, 52, 1 (2017), Jan., 775–788. issn:0362-1340 https://doi.org/10.1145/3093333.3009856
[17]
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. 2022. Gradualizing the Calculus of Inductive Constructions. ACM Transactions on Programming Languages and Systems, 44, 2 (2022), Article 7, apr, 82 pages. issn:0164-0925 https://doi.org/10.1145/3495528
[18]
Per Martin-Löf. 1972. An intuitionistic theory of types. University of Stockholm.
[19]
Conor McBride. 2000. Dependently typed functional programs and their proofs.
[20]
Conor McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs, Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, and Robert Pollack (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 197–216. isbn:978-3-540-45842-5 https://doi.org/10.1007/3-540-45842-5_13
[21]
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. SE-412 96 Göteborg, Sweden.
[22]
Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In Exploring New Frontiers of Theoretical Informatics, Jean-Jacques Levy, Ernst W. Mayr, and John C. Mitchell (Eds.). Springer US, Boston, MA. 437–450. isbn:978-1-4020-8141-5 https://doi.org/10.1007/1-4020-8141-3_34
[23]
Erik Palmgren and Viggo Stoltenberg-Hansen. 1990. Domain interpretations of martin-löf’s partial type theory. Annals of Pure and Applied Logic, 48, 2 (1990), 135–196. issn:0168-0072 https://doi.org/10.1016/0168-0072(90)90044-3
[24]
John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, B. Robinet (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 408–425. isbn:978-3-540-37819-8 https://doi.org/10.1007/3-540-06859-7_148
[25]
Steven Schäfer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving, Christian Urban and Xingyuan Zhang (Eds.). Springer International Publishing, Cham. 359–374. isbn:978-3-319-22102-1 https://doi.org/10.1007/978-3-319-22102-1_24
[26]
Jeremy Siek and Walid Taha. 2007. Gradual typing for objects. In European Conference on Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 2–27. isbn:978-3-540-73589-2 https://doi.org/10.1007/978-3-540-73589-2_2
[27]
Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 32). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 274–293. isbn:978-3-939897-80-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.SNAPL.2015.274
[28]
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich. 2012. Irrelevance, heterogeneous equality, and call-by-value dependent type systems. Mathematically Structured Functional Programming, 76 (2012), 112–162.
[29]
Vilhelm Sjöberg and Stephanie Weirich. 2015. Programming up to congruence. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 369–382. https://doi.org/10.1145/2676726.2676974
[30]
Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage migration: From scripts to programs. In ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications. https://doi.org/10.1145/1176617.1176755
[31]
Dimitrios Vytiniotis, Simon Peyton Jones, and José Pedro Magalhães. 2012. Equality Proofs and Deferred Type Errors: A Compiler Pearl. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP ’12). Association for Computing Machinery, New York, NY, USA. 341–352. isbn:9781450310543 https://doi.org/10.1145/2364527.2364554
[32]
Philip Wadler. 2015. A Complement to Blame. In 1st Summit on Advances in Programming Languages (SNAPL 2015), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 32). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 309–320. isbn:978-3-939897-80-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.SNAPL.2015.309
[33]
Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–16. isbn:978-3-642-00590-9 https://doi.org/10.1007/978-3-642-00590-9_1
[34]
Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2020. Programming Language Foundations in Agda. http://plfa.inf.ed.ac.uk/20.07/
[35]
A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), 38–94. issn:0890-5401 https://doi.org/10.1006/inco.1994.1093
[36]
Hongwei Xi. 2007. Dependent ML An approach to practical programming with dependent types. Journal of Functional Programming, 17, 2 (2007), 03, 215–286. isbn:09567968 https://doi.org/10.1017/S0956796806006216 Copyright - 2006 Cambridge University Press; Last updated - 2010-06-08
[37]
Jakub Zalewski, James McKinna, J. Garrett Morris, and Philip Wadler. 2020. λ dB: Blame tracking at higher fidelity. In Workshop on Gradual Typing (WGT20). Association for Computing Machinery, New Orleans. 171–192.
Index Terms
- A Dependently Typed Language with Dynamic Equality
Index terms have been assigned to the content through auto-classification.
Recommendations
Dependently typed programming in Agda
TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementationDependently typed languages have for a long time been used to describe proofs about programs. Traditionally, dependent types are used mostly for stating and proving the properties of the programs and not in defining the programs themselves. An ...
Bidirectional Elaboration of Dependently Typed Programs
PPDP '14: Proceedings of the 16th International Symposium on Principles and Practice of Declarative ProgrammingDependently typed programming languages allow programmers to express a rich set of invariants and verify them statically via type checking. To make programming with dependent types practical, dependently typed systems provide a compact language for ...
Propositional equality for gradual dependently typed programming
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2023
70 pages
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 August 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
TyDe '23
Sponsor:
TyDe '23: 8th ACM SIGPLAN International Workshop on Type-Driven Development
September 4, 2023
WA, Seattle, USA
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 76Total Downloads
- Downloads (Last 12 months)76
- Downloads (Last 6 weeks)2
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in