Type checker for a language with a substructural type system using scope graphs
J.G. Knapen (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Casper Bach Bach – Mentor (TU Delft - Programming Languages)
Aron Zwaan – Mentor (TU Delft - Programming Languages)
Thomas Durieux – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Substructural typing imposes additional constraints on variable usage during type checking and requires specialized approaches to ensure type soundness. In this study, we investigate the implementation of a type checker using scope graphs for languages with substructural type systems. Scope graphs, a data structure representing scoping, provide a foundation for defining type checking algorithms. Our research project extends an existing Haskell library, incorporating typing rules for non-substructural, linear, and affine type systems. Through careful examination and comparison of scope graph and calculus implementations, we evaluate their expressiveness, extensibility, and readability. While the scope graph implementation demonstrates promising results, passing all test cases, the calculus implementation encounters unification errors in a subset of the tests. We conclude that the scope graph implementation offers a solid foundation for substructural typing, with potential for easy extension and integration with other language features. However, further work is needed to develop a comprehensive test suite and address the challenges faced by the calculus implementation. By advancing these areas, we can enhance the effectiveness of substructural type checking and enable more reliable and secure programming practices in languages with substructural type systems.