Type checker for a language with a substructural type system using scope graphs

Type checker for a language with a substructural type system using scope graphs

Knapen, Jan (TU Delft Electrical Engineering, Mathematics and Computer Science)

Poulsen, C.B. (mentor)
Zwaan, A.S. (mentor)
Durieux, T. (graduation committee)

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2023-06-29

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.

Type Checker
Scope Graphs
Substructural Type Systems

http://resolver.tudelft.nl/uuid:0469a179-4228-4d30-a263-8f7e17da7026

Student theses

bachelor thesis

© 2023 Jan Knapen