Teaching Type Systems Implementation with Stella, an Extensible Statically Typed Programming Language

TL;DR

The paper addresses the challenge of teaching and practicing type system implementation by combining a minimal core language with extensible features. It proposes a pedagogy built around Stella, BNFC templates for multi-language implementations, and a structured two-part course that integrates theory from TaPL with practical typechecker development. Empirical results from 49 students across diverse languages highlight the viability of this approach while identifying practical bottlenecks such as environment setup and template coverage. The work demonstrates that an extensible educational language, paired with automated templates, can facilitate deep understanding of type systems and support scalable teaching across languages.

Abstract

We report on a half-semester course focused around implementation of type systems in programming languages. The course assumes basics of classical compiler construction, in particular, the abstract syntax representation, the Visitor pattern, and parsing. The course is built around a language Stella with a minimalistic core and a set of small extensions, covering algebraic data types, references, exceptions, exhaustive pattern matching, subtyping, recursive types, universal polymorphism, and type reconstruction. Optionally, an implementation of an interpreter and a compiler is offered to the students. To facilitate fast development and variety of implementation languages we rely on the BNF Converter tool and provide templates for the students in multiple languages. Finally, we report some results of teaching based on students' achievements.

Figures (7)

• Figure 1: Simple program in Stella Core.
• Figure 2: A Stella program featuring exceptions.
• Figure 3: Sample Stella program with structural subtyping and records.
• Figure 4: Sample Stella program with structural subtyping and variants.
• Figure 5: Sample Stella program with universal polymorphism.