Codebase Underlying the BSc Thesis: Type-Checking Modules and Imports using Scope Graphs
doi: 10.4121/288296b9-fcdf-4960-bab4-8aee3a46927c
The objective of this research was to determine whether a stratified type-checking approach using scope graphs could type-check the proof-of-concept language LM. Scope graphs provide a way to type-check real-world programming languages and their constructs. Previous implementations that type-check LM, a language with relative, unordered, and glob imports, do not halt. This dataset contains Haskell code for constructing and type-checking a scope graph of an LM program. It is based on the Phased Haskell library. With this implementation, the all test cases halt and the majority exhibit the correct behaviour with only one false-negative.
This implementation uses a five-step approach:
- Constructing a module hierarchy.
- Constructing a scope graph consisting of scopes and module sinks.
- Iteratively resolving imports and placing import edges in the scope graph.
- Adding all declarations of all modules to the scope graph.
- Type-checking the bodies of all declarations with respect to the scope graph.
Many test cases bundled with this data set are based on those for LMR (which is very similar to LM) and can be found here. On top of that. more test cases were derived and included. All test cases are denoted as annotated terms.
This data set is linked to a Bachelor's thesis completed at the EEMCS faculty at the TU Delft. A link will be added after publication.
- 2023-06-21 first online, published, posted
DATA
To access the source code, use the following command:
git clone https://data.4tu.nl/v3/datasets/2ef92305-5f55-417a-9da4-b0e50f0d265a.git
- 3,413 bytesMD5:
8004d249a5210a3596acebfcde4ee5d8
README.md - 1,561,305 bytesMD5:
fb5879f8c88d5bd58495113f5fb0e38d
lmtc.tar.gz -
download all files (zip)
1,564,718 bytes unzipped