research-article

Open access

A systematic approach to deriving incremental type checkers

Authors:

Sebastian Erdweg,

Tamás SzabóAuthors 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

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), Luís Caires (Ed.), Vol. 11423. Springer, 525-552. https://doi.org/10.1007/978-3-030-17184-1_19

[2]

Michael Arntzenius and Neel Krishnaswami. 2020. Seminaïve 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

[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

[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

[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

[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

[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

[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

[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

[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

[11]

Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press. https: //www.cs.cmu.edu/%7Erwh/pfpl/index.html

[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 Müller (Ed.), Vol. 74. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 18 : 1-18 : 26. https://doi.org/10.4230/LIPIcs.ECOOP. 2017.18

[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

[14]

Benjamin C. Pierce. 2002. Types and programming languages. MIT Press.

Digital Library

[15]

Raghu Ramakrishnan, François 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

[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

[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

[18]

Tamás Szabó, Gábor 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

[19]

Tamás Szabó, 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

[20]

Tamás Szabó, 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

[21]

Guido Wachsmuth, Gabriël 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

[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

[23]

Adrienne Watt. 2018. Database design.

Cited By

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 ProgramsProceedings 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

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 ...
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 ...
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 ...

Comments

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 © 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

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
1,667
Total Downloads

Downloads (Last 12 months)574
Downloads (Last 6 weeks)50

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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 ProgramsProceedings 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
Szabó 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 BBurgueño 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 ASzabó 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-checkersProceedings 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 SSzabó 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
Szabó 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.

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