The Statix meta-language is a domain-specific language that is used to describe specifications for type systems using high-level declarative inference rules. Type checkers
can be automatically generated from these rules, saving one from the burden of writing
it manually. One of the problems with these generated type checkers is performance;
handwritten type checkers usually outperform the generated ones. Statix uses the formalism of scope graphs to represent name binding, and querying these scope graphs is
known to be the main performance bottleneck. Improving the performance of queries
means improving the performance of the type checkers generated by Statix.

In this thesis, we propose a memoised variant of the current state-of-the-art query
resolution algorithm that memoises data encountered during graph traversal, reducing
future queries to a cache lookup. We also identify common patterns in real-world scope
graphs and link those to the name binding structure that created them. We construct a
synthetic dataset with these patterns that is used to evaluate query resolution algorithms
with microbenchmarks. This gives us more granular information on what name binding
structures benefit most, if at all, from memoisation.

The results of these benchmarks are the performance differences between the memoised algorithm and the current state-of-the-art algorithm per identified pattern. They
show that our proposed algorithm breaks even in terms of performance after only two
queries for most patterns. Furthermore, we demonstrate that our proposed algorithm
and the current state-of-the-art provide identical efficacy. The tradeoffs are twofold: the
cache increases the memory usage of query resolution significantly and the query resolution parameters were tweaked to make caching possible, but less versatile. The changed
query parameters’ limitations should only be theoretical however, the Statix specification
for Java 1.5 has 23 out of 25 fully compatible queries.

In this paper, we explore scope graphs as a formal model for constructing type checkers for programming languages that support type classes. Type classes provide a powerful mechanism for ad hoc-polymorphism and code reuse. Nevertheless, the incorporation of type classes into type checkers poses challenges, as it necessitates the resolution of instances and the assurance of coherence amidst overlapping instances. Our approach facilitates the separation of concerns between type class resolution and type checking, promoting extensibility and maintainability of the type checker. We contribute with a formal definition of scope graphs for languages with type classes, accompanied by algorithms for type class resolution and type checking. To assess the correctness of this approach, we implement a prototype type checker, and conduct experiments on a collection of representative programs. The results demonstrate the effectiveness of this baseline approach.

Scope graphs provide a way to type-check real-world programming languages and their constructs. A previous implementation that type-checks the proof-of-concept language LM, a language with relative, unordered, and glob imports, does not halt. This thesis discusses a five-step approach for constructing and type-checking a scope graph of an LM program. Using manually scheduled queries and auxiliary algorithms, type-checking the majority of examples failing in previous literature succeeds. The introduction of breadth-first-traversal and multi-origin querying is discussed as new scope graph primitives to aid in the reusability of this thesis for type-checkers that require stratified resolution.

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.

This paper investigates the viability of using scope graphs to implement type checkers for programming languages, specifically for a Scala subset. The primary objective is to determine if scope graphs can offer a declarative and extensible approach to type checking. To achieve this, we used a phased Haskell library to implement such a type checker. The declarativity and feature extensibility of the approach were evaluated by means of comparation with Rouvoet et al.'s approach in mini-Statix. The results demonstrate that using scope graphs as a basis for type checking yields a modular and extensible solution compared to traditional methods. However, it is noted that this approach may sacrifice a certain degree of declarativity. These findings suggest that scope graphs are a promising tool for type checking, particularly in the context of name binding. Further research is recommended to explore the possibility of implementing similar type checkers for other programming languages. Additionally, the paper suggests incorporating additional features into the targeted Scala subset, thereby enhancing its extensibility.

Static type systems can greatly enhance the quality of programs, but implementing a type checker for them is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of the type system. However, so far Statix has not been used to implement a type system with dependent types, an expressive class of type systems which require evaluation of terms during type checking.

In this thesis, we present a specification of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.