https://dl.acm.org/doi/10.1145/3428195 skip to main content * ACM Digital Library home * ACM Association for Computing Machinery corporate logo * Advanced Search * Browse * About * + Sign in + Register * * Advanced Search * Journals * Magazines * Proceedings * Books * SIGs * Conferences * People * * More * Search ACM Digital Library[ ] SearchSearch Advanced Search Proceedings of the ACM on Programming Languages * Journal Home * Just Accepted * Latest Issue * * Archive * Authors + Author Guidelines + Calls for Papers + PACMPL Policies + ACM Author Policies + Author List * Editors + Editorial Board + Associate Editors Welcome Video * Reviewers * Open Access + PACMPL Open Access + ACM Open Access * Award Winners * About + About PACMPL + Announcements + Abstracting/Indexing + PACMPL Affiliations * Contact Us * More * Home * ACM Journals * Proceedings of the ACM on Programming Languages * Vol. 4, No. OOPSLA * A systematic approach to deriving incremental type checkers research-article Open access Share on * * * * * * A systematic approach to deriving incremental type checkers Authors: [default-pr]Andre Pacak, [default-pr]Sebastian Erdweg, [default-pr]Tamas SzaboAuthors Info & Claims Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA Article No.: 127, Pages 1 - 28 https://doi.org/10.1145/3428195 Published: 13 November 2020 Publication History 11citation1,407Downloads Metrics Total Citations11 Total Downloads1,407 Last 12 Months422 Last 6 weeks93 Get Citation Alerts New Citation Alert added! This alert has been successfully added and will be sent to: You will be notified whenever a record that you have chosen has been cited. To manage your alert preferences, click on the button below. Manage my Alerts New Citation Alert! Please log in to your account PDFeReader * Contents Proceedings of the ACM on Programming Languages Volume 4, Issue OOPSLA PREVIOUS ARTICLE Effects as capabilities: effect handlers and lightweight effect polymorphism Previous NEXT ARTICLE Proving highly-concurrent traversals correct Next + Abstract + Supplementary Material + References ACM Digital Library * + Information & Contributors + Bibliometrics & Citations + View Options + References + Media + Tables + Share Abstract Static typing can guide programmers if feedback is immediate. Therefore, all major IDEs incrementalize type checking in some way. However, prior approaches to incremental type checking are often specialized and hard to transfer to new type systems. In this paper, we propose a systematic approach for deriving incremental type checkers from textbook-style type system specifications. Our approach is based on compiling inference rules to Datalog, a carefully limited logic programming language for which incremental solvers exist. The key contribution of this paper is to discover an encoding of the infinite typing relation as a finite Datalog relation in a way that yields efficient incremental updates. We implemented the compiler as part of a type system DSL and show that it supports simple types, some local type inference, operator overloading, universal types, and iso-recursive types. Supplementary Material Auxiliary Presentation Video (oopsla20main-p11-p-video.mp4) Static typing can guide programmers if feedback is immediate. Therefore, all major IDEs incrementalize type checking in some way. However, prior approaches to incremental type checking are often specialized and hard to transfer to new type systems. In this paper, we propose a systematic approach for deriving incremental type checkers from textbook-style type system specifications. Our approach is based on compiling inference rules to Datalog, a carefully limited logic programming language for which incremental solvers exist. The key contribution of this paper is to discover an encoding of the infinite typing relation as a finite Datalog relation in a way that yields efficient incremental updates. We implemented the compiler as part of a type system DSL and show that it supports simple types, some local type inference, operator overloading, universal types, and iso-recursive types. * Download * 165.82 MB References [1] Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, and C.-H. Luke Ong. 2019. Fixing Incremental Computation-Derivatives of Fixpoints, and the Recursive Semantics of Datalog. In Programming Languages and Systems-28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings (Lecture Notes in Computer Science), Luis Caires (Ed.), Vol. 11423. Springer, 525-552. https://doi.org/10.1007/ 978-3-030-17184-1_19 Crossref Google Scholar [2] Michael Arntzenius and Neel Krishnaswami. 2020. Seminaive evaluation for a higher-order functional language. Proc. ACM Program. Lang. 4, POPL ( 2020 ), 22 : 1-22 : 28. https://doi.org/10.1145/3371090 Digital Library Google Scholar [3] Isabelle Attali, Jacques Chazarain, and Serge Gilette. 1992. Incremental Evaluation of Natural Semantics Specification. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP'92, Leuven, Belgium, August 26-28, 1992, Proceedings (Lecture Notes in Computer Science), Maurice Bruynooghe and Martin Wirsing (Eds.), Vol. 631. Springer, 87-99. https://doi.org/10.1007/3-540-55844-6_129 Crossref Google Scholar [4] Catriel Beeri and Raghu Ramakrishnan. 1991. On the Power of Magic. J. Log. Program. 10, 3 & 4 ( 1991 ), 255-299. https: //doi.org/10.1016/ 0743-1066 ( 91 ) 90038-Q Digital Library Google Scholar [5] Matteo Busi, Pierpaolo Degano, and Letterio Galletta. 2019. Using Standard Typing Algorithms Incrementally. In NASA Formal Methods-11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings (Lecture Notes in Computer Science), Julia M. Badger and Kristin Yvonne Rozier (Eds.), Vol. 11460. Springer, 106-122. https: / /doi.org/10.1007/978-3-030-20652-9_7 Crossref Google Scholar [6] Thierry Despeyroux. 1984. Executable Specification of Static Semantics. In Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings (Lecture Notes in Computer Science), Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin (Eds.), Vol. 173. Springer, 215-233. https:// doi.org/10.1007/3-540-13346-1_11 Crossref Google Scholar [7] Sebastian Erdweg, Oliver Bracevac, Edlira Kuci, Matthias Krebs, and Mira Mezini. 2015. A co-contextual formulation of type rules and its application to incremental type checking. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 880-897. https://doi.org/10.1145/ 2814270. 2814277 Digital Library Google Scholar [8] Frantisek Farka, Ekaterina Komendantskaya, and Kevin Hammond. 2018. Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. Theory Pract. Log. Program. 18, 3-4 ( 2018 ), 484-501. https://doi.org/10.1017/ S1471068418000212 Crossref Google Scholar [9] Luca Franceschini, Davide Ancona, and Ekaterina Komendantskaya. 2016. Structural Resolution for Abstract Compilation of Object-Oriented Languages. In Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty 2016, Edinburgh, UK, 28-29 November 2016 (EPTCS), Ekaterina Komendantskaya and John Power (Eds.), Vol. 258. 19-35. https://doi.org/10.4204/EPTCS.258.2 Crossref Google Scholar [10] Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini. 2015. Type systems for the masses: deriving soundness proofs and eficient checkers. In 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2015, Pittsburgh, PA, USA, October 25-30, 2015, Gail C. Murphy and Guy L. Steele Jr. (Eds.). ACM, 137-150. https://doi.org/10.1145/ 2814228.2814239 Digital Library Google Scholar [11] Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press. https: //www.cs.cmu.edu/ %7Erwh/pfpl/index.html Google Scholar [12] Edlira Kuci, Sebastian Erdweg, Oliver Bracevac, Andi Bejleri, and Mira Mezini. 2017. A Co-contextual Type Checker for Featherweight Java. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain (LIPIcs), Peter Muller (Ed.), Vol. 74. Schloss Dagstuhl-Leibniz-Zentrum fur Informatik, 18 : 1-18 : 26. https://doi.org/10.4230/LIPIcs.ECOOP. 2017.18 Crossref Google Scholar [13] Lambert G. L. T. Meertens. 1983. Incremental Polymorphic Type Checking in B. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, John R. Wright, Larry Landweber, Alan J. Demers, and Tim Teitelbaum (Eds.). ACM Press, 265-275. https://doi.org/10.1145/ 567067.567092 Digital Library Google Scholar [14] Benjamin C. Pierce. 2002. Types and programming languages. MIT Press. Digital Library Google Scholar [15] Raghu Ramakrishnan, Francois Bancilhon, and Abraham Silberschatz. 1987. Safety of Recursive Horn Clauses With Infinite Relations. In Proceedings of the Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 23-25, 1987, San Diego, California, USA, Moshe Y. Vardi (Ed.). ACM, 328-339. https://doi.org/ 10.1145/28659.28694 Digital Library Google Scholar [16] Leonid Ryzhyk and Mihai Budiu. 2019. Diferential Datalog. In Datalog 2.0 2019-3rd International Workshop on the Resurgence of Datalog in Academia and Industry co-located with the 15th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2019) at the Philadelphia Logic Week 2019, Philadelphia, PA (USA), June 4-5, 2019 (CEUR Workshop Proceedings), Mario Alviano and Andreas Pieris (Eds.), Vol. 2368. CEUR-WS.org, 56-67. http://ceurws.org/ Vol-2368 /paper6.pdf Google Scholar [17] Yannis Smaragdakis and Martin Bravenboer. 2010. Using Datalog for Fast and Easy Program Analysis. In Datalog Reloaded-First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised Selected Papers (Lecture Notes in Computer Science), Oege de Moor, Georg Gottlob, Tim Furche, and Andrew Jon Sellers (Eds.), Vol. 6702. Springer, 245-251. https://doi.org/10.1007/978-3-642-24206-9_14 Digital Library Google Scholar [18] Tamas Szabo, Gabor Bergmann, Sebastian Erdweg, and Markus Voelter. 2018a. Incrementalizing lattice-based program analyses in Datalog. PACMPL 2, OOPSLA ( 2018 ), 139 : 1-139 : 29. https://doi.org/10.1145/ 3276509 Digital Library Google Scholar [19] Tamas Szabo, Sebastian Erdweg, and Markus Voelter. 2016. IncA: a DSL for the definition of incremental program analyses. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, David Lo, Sven Apel, and Sarfraz Khurshid (Eds.). ACM, 320-331. https://doi.org/ 10.1145/2970276. 2970298 Digital Library Google Scholar [20] Tamas Szabo, Edlira Kuci, Matthijs Bijman, Mira Mezini, and Sebastian Erdweg. 2018b. Incremental overload resolution in object-oriented programming languages. In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, ISSTA 2018, Amsterdam, Netherlands, July 16-21, 2018, Julian Dolby, William G. J. Halfond, and Ashish Mishra (Eds.). ACM, 27-33. https://doi.org/10.1145/3236454.3236485 Digital Library Google Scholar [21] Guido Wachsmuth, Gabriel D. P. Konat, Vlad A. Vergu, Danny M. Groenewegen, and Eelco Visser. 2013. A Language Independent Task Engine for Incremental Name and Type Analysis. In Software Language Engineering-6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings (Lecture Notes in Computer Science), Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.), Vol. 8225. Springer, 260-280. https://doi.org/10.1007/ 978-3-319-02654-1_15 Crossref Google Scholar [22] Philip Wadler. 1990. Deforestation: Transforming Programs to Eliminate Trees. Theor. Comput. Sci. 73, 2 ( 1990 ), 231-248. https:/ /doi.org/10.1016/ 0304-3975 ( 90 ) 90147-A Digital Library Google Scholar [23] Adrienne Watt. 2018. Database design. Google Scholar Cited By View all * Krishna SLal APavlogiannis ATuppe O(2024)On-the-Fly Static Analysis via Dynamic Bidirected Dyck ReachabilityProceedings of the ACM on Programming Languages10.1145/36328848:POPL(1239-1268) Online publication date: 5-Jan-2024 https://dl.acm.org/doi/10.1145/3632884 * Sahebolamri ABarrett LMoore SMicinski K(2023)Bring Your Own Data Structures to DatalogProceedings of the ACM on Programming Languages10.1145/36228407:OOPSLA2(1198-1223)Online publication date: 16-Oct-2023 https://dl.acm.org/doi/10.1145/3622840 * Pacak AErdweg S(2023)Interactive Debugging of Datalog Programs Proceedings of the ACM on Programming Languages10.1145/36228247 :OOPSLA2(745-772)Online publication date: 16-Oct-2023 https://dl.acm.org/doi/10.1145/3622824 * Show More Cited By Index Terms 1. A systematic approach to deriving incremental type checkers 1. Theory of computation 1. Logic 1. Constraint and logic programming 2. Semantics and reasoning 1. Program constructs 1. Type structures 2. Program reasoning 1. Program analysis Recommendations * Incremental type-checking for free: using scope graphs to derive incremental type-checkers Fast analysis response times in IDEs are essential for a good editor experience. Incremental type-checking can provide that in a scalable fashion. However, existing techniques are not reusable between languages. Moreover, mutual and dynamic dependencies ... Read More * Incremental type-checking for type-reflective metaprograms GPCE '10: Proceedings of the ninth international conference on Generative programming and component engineering Garcia introduces a calculus for type-reflective metaprogramming that provides much of the power and flexibility of C++ templates and solves many of its problems. However, one of the problems that remains is that the residual program is not type checked ... Read More * Type systems for the masses: deriving soundness proofs and efficient checkers Onward! 2015: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!) The correct definition and implementation of non-trivial type systems is difficult and requires expert knowledge, which is not available to developers of domain-specific languages (DSLs) in practice. We propose Veritas, a workbench that simplifies the ... Read More 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 4, Issue OOPSLA November 2020 3108 pages EISSN:2475-1421 DOI:10.1145/3436718 Issue's Table of Contents Copyright (c) 2020 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: 13 November 2020 Published in PACMPL Volume 4, Issue OOPSLA Permissions Request permissions for this article. Request Permissions Check for updates Author Tags 1. datalog 2. incremental type checking 3. type system transformation Qualifiers * Research-article Contributors [loader-7e6] Other Metrics View Article Metrics Bibliometrics & Citations Bibliometrics Article Metrics * 11 Total Citations View Citations * 1,407 Total Downloads * Downloads (Last 12 months)422 * Downloads (Last 6 weeks)93 Reflects downloads up to 30 Aug 2024 Other Metrics View Author Metrics Citations Cited By View all * Krishna SLal APavlogiannis ATuppe O(2024)On-the-Fly Static Analysis via Dynamic Bidirected Dyck ReachabilityProceedings of the ACM on Programming Languages10.1145/36328848:POPL(1239-1268) Online publication date: 5-Jan-2024 https://dl.acm.org/doi/10.1145/3632884 * Sahebolamri ABarrett LMoore SMicinski K(2023)Bring Your Own Data Structures to DatalogProceedings of the ACM on Programming Languages10.1145/36228407:OOPSLA2(1198-1223)Online publication date: 16-Oct-2023 https://dl.acm.org/doi/10.1145/3622840 * Pacak AErdweg S(2023)Interactive Debugging of Datalog Programs Proceedings of the ACM on Programming Languages10.1145/36228247 :OOPSLA2(745-772)Online publication date: 16-Oct-2023 https://dl.acm.org/doi/10.1145/3622824 * Szabo TChandra SBlincoe KTonella P(2023)Incrementalizing Production CodeQL AnalysesProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3613860 (1716-1726)Online publication date: 30-Nov-2023 https://dl.acm.org/doi/10.1145/3611643.3613860 * Zwaan AFischer BBurgueno LCazzola W(2022)Specializing Scope Graph Resolution QueriesProceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering10.1145/ 3567512.3567523(121-133)Online publication date: 29-Nov-2022 https://dl.acm.org/doi/10.1145/3567512.3567523 * Pacak ASzabo TErdweg SScholz BKameyama Y(2022)Incremental Processing of Structured Data in DatalogProceedings of the 21st ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3564719.3568686(20-32)Online publication date: 29-Nov-2022 https://dl.acm.org/doi/10.1145/3564719.3568686 * Zwaan Avan Antwerpen HVisser E(2022)Incremental type-checking for free: using scope graphs to derive incremental type-checkers Proceedings of the ACM on Programming Languages10.1145/35633036 :OOPSLA2(424-448)Online publication date: 31-Oct-2022 https://dl.acm.org/doi/10.1145/3563303 * Li YSatya KZhang Q(2022)Efficient algorithms for dynamic bidirected Dyck-reachabilityProceedings of the ACM on Programming Languages10.1145/34987246:POPL(1-29)Online publication date: 12-Jan-2022 https://dl.acm.org/doi/10.1145/3498724 * Erdweg SSzabo TPacak AFreund SYahav E(2021)Concise, type-safe, and efficient structural diffingProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454052(406-419)Online publication date: 19-Jun-2021 https://dl.acm.org/doi/10.1145/3453483.3454052 * Szabo TErdweg SBergmann GFreund SYahav E(2021)Incremental whole-program analysis in Datalog with latticesProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454026(1-15)Online publication date: 19-Jun-2021 https://dl.acm.org/doi/10.1145/3453483.3454026 * Show More Cited By View Options View options PDF View or Download as a PDF file. PDF eReader View online with eReader. eReader 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 Full Access Get this Article Media Figures Other Tables Share Share Share this Publication link Copy Link Copied! Copying failed. Share on social media XLinkedInRedditFacebookemail Affiliations [default-pr] Andre Pacak University of Mainz, Germany View Profile [default-pr] Sebastian Erdweg University of Mainz, Germany View Profile [default-pr] Tamas Szabo University of Mainz, Germany / itemis, Germany View Profile Download PDF Go to Go to Show all references Request permissionsExpand All Collapse Expand Table Authors Info & Affiliations View Issue's Table of Contents Export Citations Select Citation format[BibTeX ] * Please download or close your previous search result export first before starting a new bulk export. Preview is not available. By clicking download,a status dialog will open to start the export process. The process may takea few minutes but once it finishes a file will be downloadable from your browser. You may continue to browse the DL while the export process is in progress. Download + Download citation + Copy citation Footer Categories * Journals * Magazines * Books * Proceedings * SIGs * Conferences * Collections * People About * About ACM Digital Library * ACM Digital Library Board * Subscription Information * Author Guidelines * Using ACM Digital Library * All Holdings within the ACM Digital Library * ACM Computing Classification System * Accessibility Statement Join * Join ACM * Join SIGs * Subscribe to Publications * Institutions and Libraries Connect * Contact us via email * ACM on Facebook * ACM DL on X * ACM on Linkedin * Send Feedback * Submit a Bug Report The ACM Digital Library is published by the Association for Computing Machinery. Copyright (c) 2024 ACM, Inc. * Terms of Usage * Privacy Policy * Code of Ethics ACM Digital Library home ACM Association for Computing Machinery corporate logo Your Search Results Download Request We are preparing your search results for download ... We will inform you here when the file is ready. Download now! Your Search Results Download Request Your file of search results citations is now ready. Download now! Your Search Results Download Request Your search export query has expired. Please try again.