tella]stellafontsize= otlin]kotlinfontsize=

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

Abdelrahman Abounegm Nikolai Kudasov Alexey Stepanov Lab of Programming
Languages and Compilers
Innopolis University
Innopolis, Tatarstan Republic, Russia<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### 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.

##  1 Introduction

Type systems constitute an important part of most modern programming
languages, from Java and C++ to Python and TypeScript to Scala and Haskell, to
mention a few. When using static types, programmers devote a significant part
of their interaction with the compiler or a static analysis tool working
through the type errors. Type-Driven Development (TyDD) [10] goes even further
and suggests writing the types first and then follow the types to produce an
implementation. Among popular modern programming languages, expressive type
systems are becoming more widespread. Two recent examples include Rust [24], a
systems programming language with ownership types, and Differentiable Swift
[37], a dialect of Swift with differentiable types. Such languages incorporate
quite elaborate type system features that require solid understanding of the
basics to be used efficiently.

Type systems are not only used in compilers, but also in proof assistants such
as Agda, Coq, and Isabelle/HOL. These usually rely on dependent type systems,
such as Martin-Löf Type Theory [23] or Calculus of Constructions [11]. Using
proof assistants for mathematics or program verification is somewhat similar
in practice to TyDD in programming languages: in both cases the user of the
system spends a significant amount of time dealing with type errors.

Although linters and good error messages help with type errors, it is
important for the users to understand and be able to follow typing rules to
productively resolve the issues and utilize type checker as a helping tool,
instead of seeing it as a barrier. Although courses in statically typed
programming languages help teach students some of the mechanics behind type
checking, we believe a first-hand experience in the implementation of a type
system deepens that understanding while also allowing students to apply some
of those types in the implementation. Unfortunately, existing compilers
construction courses appear to either provide an overview of the compiler
pipeline, resort to a simplified semantic analysis phase, focus on the code
generation phase, or work with a low-level intermediate representation such as
LLVM IR or Java bytecode.

On the other hand, courses that focus on type systems often offer
implementation of a variant of typed lambda calculus, which appears to
disengage some students who are used to Java-style or Python-style syntax of
programming languages and who do not have sufficient experience with
functional programming. In particular, in a previous iteration of our course,
many students found it quite difficult and unintuitive to program or even read
programs in lambda calculus, whereas rewriting a lambda expression in Python
using explicit function definitions helped them navigate the operational
semantics of lambda calculus.

While lambda calculus is too raw, any modern programming language is too
complex. Indeed, even the core of most modern languages is too complex to give
as an implementation exercise for students. The Haskell programming language,
and in particular its implementation in the Glasgow Haskell Compiler (GHC),
comes close to a language with a small core: it employs a system of language
extensions that allows to enrich the language per module. In this work, we are
inspired by this approach and design a language with a very small fixed core
that is easy to implement for students, and provide various extensions for
further developments.

To be able to focus on the type checking, it is not enough to assume that
students have already mastered the lexical and syntactical analyzers.
Implementing those with proper types for the abstract syntax tree from scratch
still requires significant time. Luckily, at least for simple languages, there
is a good selection of tools that can do that automatically, such as XText
[13] and BNF Converter [14]. In our course, we rely heavily on BNF Converter
to offer templates in multiple languages and encourage diversity of
implementations in student submissions.

###  1.1 Related Work

The idea of designing a programming language specifically for teaching
compiler construction is not new. One of the first such languages was
MINIPASCAL, a simplified version of Pascal programming language, introduced by
Appelbe [6].

More recently, Berezun and Boulytchev [7] reported on the use of the
programming language
$\lambda\kern-1.66702pt\lower-2.15277pt\hbox{$a$}\kern-1.00006pt\lower
0.86108pt\hbox{$\mathcal{M}$}\kern-1.00006pt\lower-2.15277pt\hbox{$a$}$111https://github.com/PLTools/Lama,
developed by JetBrains Research for educational purposes, in their
introductory course on compilers. They asked students to implement a compiler
of $\lambda\kern-1.66702pt\lower-2.15277pt\hbox{$a$}\kern-1.00006pt\lower
0.86108pt\hbox{$\mathcal{M}$}\kern-1.00006pt\lower-2.15277pt\hbox{$a$}$ in
itself, a procedural language with first-class functions that is untyped
(meaning no _static_ type checking is performed). It appears that the choice
to make the language untyped was to afford simpler implementations. Thus,
Berezun and Boulytchev’s course focuses on parsing, basic semantic analysis,
and code generation. In contrast, our course focuses on type systems and puts
semantics first.

Aiken [2] introduced the Cool language, which is largely inspired by Java and
features a static type system and automatic memory management. Cool’s type
system is nominal, without support for generics, anonymous objects, or higher-
order functions, and thus does not present significant challenges in the
implementation of type checking compared to the structural type system
featured in our course.

Although basic typechecking can be covered in regular compilers courses, some
courses still specialize specifically on type systems and type checking.
Ortin, Zapico, and Cueva [30] teach design patterns helpful for implementing a
type checker in object-oriented languages.

Lübke, Fuger, Bahnsen, Billerbeck, and Schupp [20] show how to automate exams
and assignments for functional programming that include proofs traditionally
performed on paper. With Stella’s system of extensions, we have the basis for
similar automation for our assignments, but we keep advanced automation for
future work.

###  1.2 Contribution

In this paper, we report on a half-semester course on the implementation of
type systems. More specifically:

  1. 1.

In Section 2, we overview the Stella language, consisting of a minimalistic
purely functional core and a set of extensions, matching multiple topics
covered by Pierce in his book [32].

  2. 2.

In Section 3, we specify our approach to template solutions, allowing students
to get started with implementations in any of a multitude of languages,
including C++, Java, Kotlin, OCaml, TypeScript, Swift, Rust, Go, and Python.

  3. 3.

In Section 4, we outline the course structure and identify both practical and
theoretical tasks for the students. Here, we also evaluate the course based on
students’ performance.

##  2 Overview of the Stella Language

We have designed and implemented the Stella222Statically Typed Extensible
Language for Learning Advanced compiler construction (type systems) language
specifically for the purposes of teaching type systems implementation
following Pierce’s book [32]. In this section, we highlight the main design
decisions behind the Stella language and outline its main features.

Stella is a statically-typed expression-based language. It consists of a
minimalistic core language and a set of extensions. Making language extensions
explicit is advantageous in several ways:

  1. 1.

Students can quickly learn the core, explicitly see a list of features used in
every example program, and know where to look for corresponding documentation;

  2. 2.

Test programs explicitly specify the language extensions used, making it easy
to understand which features (or combinations of features) are supported by a
student’s implementation;

  3. 3.

Students can ignore extension pragmas, implicitly supporting any given set of
extensions, simplifying implementations;

  4. 4.

More extensions can be added to Stella in the future.

The canonical implementation of Stella supports all extensions. Templates
provided to the students also support all extensions, meaning that the
abstract syntax types are provided for the full language. Although this
slightly complicates the types for the core language (e.g. students have to
deal with a list of function arguments instead of a single argument), we find
that in practice students do not have any major issues with this.

A program in Stella always consists of a single file since a module system is
out of the scope of the course as it adds unnecessary complexity while not
adding much to the typechecking part of the compiler.

Below, we describe the core part of the language and the main extensions
featured in the course.

###  2.1 Stella Core

The core language of Stella is essentially a simply-typed functional
programming language, based on Programming Computable Functions (PCF) [33],
except having a syntax inspired particularly by Rust [24], and reasonably
understandable to many programmers. In fact, one of the main motivations for
Stella was the fact that many students struggled with the _syntax_ of
$\lambda$-calculus but many examples were better understood (and students came
up more easily with their own examples) when moving to a more familiar syntax
of pseudocode or Python, Java, TypeScript.

Stella Core also corresponds to simply-typed lambda calculus [32, §9] with two
base types (natural numbers and booleans) [32, §11.1].

Importantly, Stella Core supports first class functions. We justify support
for higher-order functions from the start by asking students to only implement
a typechecker, leaving the overview of possible implementations for a proper
compiler for a functional language to a later part of the course. Indeed,
while a compiler might need to deal explicitly with closures and renaming of
bound variables, in a typechecker (without extensions like universal
polymorphism or dependent types) handling of scopes is straightforward and is
not affected by the presence of higher-order functions. At the same time,
allowing higher-order functions allows us to immediately introduce more
sophisticated test programs.

⬇

// sample program in Stella Core

language core;

\parfn increment_twice(n : Nat) -> Nat {

return succ(succ(n))

}

\parfn main(n : Nat) -> Nat {

return increment_twice(succ(n))

}

Figure 1: Simple program in Stella Core.

A sample program in Stella Core is given in Fig. 1:

  1. 1.

Line 1 is a comment line; all comments in Stella start with //; there are no
multiline comments in Stella;

  2. 2.

Line 2 specifies that we are using just Stella Core (without any extensions);
it is mandatory to specify the language in the first line of a Stella program;

  3. 3.

Line 4 declares a function increment_twice with a single argument n of type
Nat and return type Nat; in Stella Core, all functions are single-argument
functions;

  4. 4.

In Line 5, return …; is a mandatory part of every function; in Stella Core
each function can only return some expression; there are no assignments,
operators, or other statements possible;

  5. 5.

In Line 5, succ(n) is an expression meaning $n+1$ (the successor of $n$);

  6. 6.

Line 8 declares a function main with a single argument n of type Nat and
return type Nat; in a Stella program there must always be a main function
declared at the top-level; the argument type and return type of main can be
specified to be any valid types;

  7. 7.

In Line 9, increment_twice(succ(n)) is an expression meaning “call
increment_twice with the argument succ(n)”.

###  2.2 Extensions

Stella supports a number of language extensions, which can be enabled with an
extend with pragma, containing a list of extension names separated by commas.
Each extension may add new syntax, typing rules, or other capabilities to the
language. Following Pierce [32], we separate _Simple Extensions_ from some
more advanced type system extensions. However, we also separate _Syntactic
Sugar and Derived Forms_ and _Base Types_ into standalone categories.

In general, each extension is supposed to be small enough to be implemented
either as a single exercise or at most as a standalone assignment. For
example, each base type has its own extension. Some extensions have simple and
generalized versions. For instance, #tuples generalizes #pairs by allowing
arbitrary size and #variants generalizes #sum-types.

####  2.2.1 Syntactic Sugar and Derived Forms

This category contains language extensions that _may_ be implemented as
derived forms, reducing them to other features of Stella. However, this is not
enforced and students are allowed to implement these extensions as standalone
features. Some notable extensions in this category include let-bindings,
nested function declarations, multiparameter functions, automatic currying,
and type ascriptions.

A simple, but important extension is sequencing. Coupled with effectful
expressions (such as mutable references), this enables imperative programming
features.

####  2.2.2 Nested Pattern Matching

Some extensions (such as sum types or variants) naturally come equipped with
pattern matching constructions. However, by default they do not allow nested
patterns, to simplify implementation and first example. _Nested_ pattern
matching is available via the #structural-patterns extension. This extension
allows nesting and combining patterns that are enabled by other extensions.
Nested patterns complicate _pattern-match coverage checking_ (also known as
_exhaustiveness checking_) even just in presence of both tuples and variants
and although it is a well-studied problem [19, 22, 35] we leave the
implementation of the exhaustiveness checker out of the scope of our course
and only ask for exhaustiveness checks without nested patterns.

####  2.2.3 Simple Types

The simple types correspond directly to Pierce’s _Simple Extensions_ [32,
§11.2, §11.6–11.10, §11.12] and include the Unit type, pairs, tuples, records,
sum types, variants, and (built-in) lists.

Importantly, all these types are _structural_ rather than _nominal_ [32,
§19.3].

####  2.2.4 References

Stella introduces references following Pierce [32, §13]. Without any ownership
types, this does not introduce any complications in the typechecking.

####  2.2.5 Exceptions

Following Pierce [32, §14], we introduce support for different treatment of
exceptions in Stella:

  1. 1.

First, simple (unrecoverable) errors [32, §14.1] are supported in the panic!
expression, enabled through #panic extension;

  2. 2.

To throw and catch exceptions carrying values [32, §14.3], the extension
#exceptions is used. To specify the type of values in exceptions, the user has
a choice:

    1. (a)

One option allows user to fix the type of values carried by exceptions. This
is achieved with the #exception-type-declaration extension and requires a
specification of exception type:

⬇

// use error codes for exceptions

exception type = Nat

// use a fixed variant type for exceptions

exception type = <| error_code : Nat, good : Bool |>

Fig. 2 provides an example of a complete Stella program that features
exceptions.

    2. (b)

Another option is to use open variant type for exceptions (OCaml-style). This
is achieved with the #open-variant-exceptions extension and allows adding
variants to the exception as needed. The following two declarations are
equivalent to the explicit variant type above, except, with open variant, it
can also be extended with more variants later:

⬇

exception variant error_code : Nat

exception variant good : Bool

⬇

language core;

\parextend with #exceptions, #exception-type-declaration;

\parexception type = Nat

\parfn fail(n : Nat) -> Bool {

return throw(succ(0))

}

\parfn main(n : Nat) -> Bool {

return try { fail(n) } with { false }

}

Figure 2: A Stella program featuring exceptions.

At the moment, Stella does not support any annotations that would specify the
possible exceptions thrown by a function.

####  2.2.6 Subtyping

Stella supports structural subtyping, following Pierce [32, §15]. The
subtyping mechanism is enabled with the #structural-subtyping extension and
interacts with other enabled extensions, such as #records and #variants.

In Fig. 3 on line 10, the function getX is applied to a record of type x :
Nat, y : Nat. Since this type is a subtype of x : Nat, it is accepted when
structural subtyping is enabled. Similarly, in Fig. 4 on line 17, the function
inc is applied to a value of variant type ¡— value : Nat —¿. Since this type
is a subtype of ¡— value : Nat, failure : Unit —¿, it is accepted when
structural subtyping is enabled.

Subtyping for function types is enabled automatically and presents a challenge
for students, since it requires them to properly understand the idea of
covariant and contravariant subtyping. We find this also to be one of the most
valuable learning points for the students, since even without typing, these
concepts are important in programming.

⬇

language core;

\parextend with #records, #structural-subtyping;

\parfn getX(r : {x : Nat}) -> Nat {

return r.x

}

\parfn main(n : Nat) -> Nat {

return getX({x = n, y = n});

}

Figure 3: Sample Stella program with structural subtyping and records.

⬇

language core;

\parextend with #variants, #structural-subtyping;

\parfn inc(r : <| value : Nat, failure : Unit |>) -> Nat {

return match r {

<| value = n |> => succ(n)

| <| failure = _ |> => 0

}

}

\parfn just(n : Nat) -> <| value : Nat |> {

return <| value = n |>

}

\parfn main(n : Nat) -> Top {

return inc(just(n));

}

Figure 4: Sample Stella program with structural subtyping and variants.

Additional extensions introduce Top and Bot (short for “Bottom”) types as
well. The Top type is the supertype of all types, while the Bot type is the
subtype of all types. The Top type is not very useful on its own, so is
normally used in combination with the #type-cast extension, which adds the
¡expression¿ cast as ¡type¿ expression syntax. This operator performs
downcasting of the expression to the specified type, which only works if the
expression was already of a supertype of the specified type.

Stella does not currently support intersection or union types [32, §15.7].

####  2.2.7 Universal Polymorphism

Universal types [32, §23] are implemented in Stella in the form of generic
functions that accept type arguments. This is enabled by the #universal-types
extension. To declare a generic function, one needs to add the generic keyword
before fn and add a type parameter list after the function name. The type
parameters are a comma-separated list of type variables enclosed in square
brackets. When invoking a generic function, the type arguments must be
provided in square brackets after the function name.

Fig. 5 shows a sample program with universal polymorphism:

  1. 1.

In Line 5, we declare function id that is parametrized by type T;

  2. 2.

In Line 10, we apply the function id to an argument, explicitly instantiating
the type parameter to Nat.

Fig. 6 features a universally polymorphic anonymous function:

  1. 1.

In Line 5, we declare the function const that returns a parametrically
polymorphic function of type forall Y. fn(Y) -¿ X;

  2. 2.

In Line 6, we construct an anonymous function of said type;

  3. 3.

In Line 10, we first instantiate the type parameter of const to Nat, then pass
x argument to get a parametrically polymorphic function of type forall Y.
fn(Y) -¿ Nat as a result. Finally, we instantiate Y with Bool and pass false
as an argument.

⬇

language core;

\parextend with #universal-types;

\pargeneric fn id[T](x : T) -> T {

return x

}

\parfn main(x : Nat) -> Nat {

return id[Nat](x)

}

Figure 5: Sample Stella program with universal polymorphism.

⬇

language core;

\parextend with #universal-types;

\pargeneric fn const[X](x : X) -> forall Y. fn(Y) -> X {

return generic [Y] fn(y : Y) { return x }

}

\parfn main(x : Nat) -> Nat {

return const[Nat](x)[Bool](false)

}

Figure 6: Sample Stella program with a universally polymorphic anonymous
function.

Currently, Stella does not support any form of bounded quantification [32,
§26], as a half semester course does not have enough room to explore this
important topic in details. However, the topic is briefly mentioned in the
lectures. In particular, the undecidability of type reconstruction in presence
of bounded quantification [32, §28.5.5] is discussed.

The #universal-types extension enables unrestricted impredicative universal
types as in System F [15, 34]. The following example demonstrates
impredicativity through self-application of f to itself:

⬇

generic fn self_app[X](f : forall X . fn(X) -> X) -> forall X . fn(X) -> X {

return f[forall X . fn(X) -> X](f)

}

In the future, we aim to support various kinds of universal polymorphism in
Stella, at least allowing for Hindley-Milner-style, predicative, and bounded
quantification (parametric polymorphism with subtyping) [32, §26].

####  2.2.8 Recursive Types

Recursive types [32, §20] (specifically, _iso-recursive types_) are
technically implemented in Stella, but not used in the course. The reason for
that is that most programming languages rely on nominal typing to provide
recursion in types. Thus, in the course, we discuss recursive types in
theoretical materials, but do not offer implementation of this part of Stella.

###  2.3 Accessibility: Documentation and Interactive Playground

To provide the students with a convenient way to learn the language and its
extensions, we have created a website with documentation and an interactive
playground. The website is available at https://fizruk.github.io/stella/.

Figure 7: Stella documentation and playground.

The documentation is written in Markdown and is compiled to HTML using MkDocs
333https://www.mkdocs.org. The browser version of the Stella interpreter is
compiled using GHCJS [29] and Miso framework444https://github.com/dmjio/miso,
which allow us to compile Haskell code to JavaScript and run it in the
browser. The playground consists of a CodeMirror555https://codemirror.net/
code editor with custom syntax highlighting using
Highlight.js666https://highlightjs.org/. The playground includes an input
field which acts as the main function argument, and an output field which
displays the result of the main function or the compilation errors (if any).

Additionally, a VS Code extension is available for Stella, which provides
syntax highlighting and snippets for the language777https://github.com/IU-
ACCPA-2023/vscode-stella/.

##  3 Implementation Templates and Typechecker Structure

By design, students are free to select any implementation language in the
course. To facilitate with implementations in many languages and avoid eating
up the time for parsing, abstract syntax implementation, and pretty-printing,
we provide students with an EBNF grammar, suitable for the BNF Converter tool
[14]. See Section 4 for the course setup, where we explain the prerequisites
allowing us to have a fast setup and skip a major part of the frontend for the
student implementation. The tool allows us to generate a lot of structure in
many languages, including Haskell, OCaml, Java, and C++. To reach even more
languages, we have leveraged the Java ANTLR backend of BNFC to produce ANTLR
grammar with Java code snippets. We then manually removed the Java code from
the ANTLR grammar and added extra annotations to provide a language-agnostic
ANTLR file888see, for instance, https://github.com/IU-ACCPA-2023/stella-
implementation-in-swift/blob/main/Sources/stella-implementation-in-
swift/Stella/stellaParser.g4. Using ANTLR backends for other languages and
writing down some definitions and conversions, we have been able to get decent
templates for more languages, including Rust, Swift, and TypeScript.

###  3.1 A Zoo of Implementation Languages

For convenience of students, we have prepared project
templates999https://github.com/IU-ACCPA-2023 in several programming languages.
The templates allow to immediately proceed with the solution of the course
objectives (implementation of typecheckers), without spending extra time on
the implementation of lexer and parser, definition of the abstract syntax, or
implementing a pretty-printer. The templates were prepared for the following
languages: C++, Java, OCaml, Python, Rust, Go. During the course, at the
request of the students, and with their help, the following languages were
added to the list: Kotlin, Swift, TypeScript, Haskell.

In the course, each student selects an implementation language, creates a copy
of a suitable template, completes the coding exercises, and submits the
solution via GitHub Classroom (by pushing to the remote repository created for
a particular assignment).

The templates were initially designed with the following structure, mostly
provided by BNFC:

  1. 1.

A grammar file (Labelled BNF grammar) describing the Stella language;

  2. 2.

Lexer and parser generated by the BNFC tool based on the grammar file;

  3. 3.

The types (e.g. classes) for the abstract syntax of Stella;

  4. 4.

A generated skeleton for recursive traversal of the abstract syntax;

  5. 5.

The main project file, which contains the functionality to read Stella source
and convert it to AST;

  6. 6.

A Makefile to compile and run the project;

  7. 7.

Some tests to verify the success of building and running the project.

At the start of the course, we found out that many students are not
comfortable enough with Make, so we have accommodated for more IDE-friendly
setups, relying on language-specific build systems, such as CMake for C++,
Dune for OCaml, and Maven for Java.

The Kotlin template is based on the Java pattern, meaning that the parser is
implemented using Java classes. However, the interpreter code is written in
Kotlin and the build system has been replaced by Gradle.

The ANTLR grammar produced by BNFC for the Java backend was used as the basis
to accommodate templates for more languages. It was manually rewritten into a
language-agnostic form (removing Java code, adding labels for rules, and
slightly modifying the structure of the grammar). We then leveraged ANTLR to
generate the _context types_ for concrete syntax tree and manually added types
for abstract syntax together with corresponding conversion functions for each
of the extra languages.

##  4 Course Structure

In this section, we discuss the organization of the course, its materials, the
instruments used, and the results of the course.

The course consists of two lectures and two lab sessions each week for a total
of 15 lectures and 15 labs over the course of eight weeks. There are 4 coding
and 3 theoretical assignments in the course, as well as an optional oral exam
at the end of the course. The first 6 weeks of the course cover type systems
following Pierce [32, §8–23], and the last 2 weeks cover implementation
details for lazy functional languages, following Peyton Jones [18, §1–5].

The course is focused on the study of type systems, their properties and
implementation. For the theoretical part of the course, students are expected
to learn about type safety, canonical representation, normalization, and be
able to prove these properties for simple type systems. The practical part
consists of implementing a type checker for Stella with a subset of
extensions. Since many of the students taking the course already have
experience with statically typed languages like Java, C#, C++, Scala, Kotlin,
Go, Dart, and TypeScript, an implicit additional objection of the course is to
help students better understand and utilize type system features in those
languages, as well as appreciate the diversity of type systems and practical
choices made by designers of those systems.

###  4.1 Prerequisites

For the most part, the course emphasizes a detailed study of a specific
component of compilers - the type checker. Our course immediately follows
another half-semester introductory course on compiler construction, during
which students developed the skills to construct their own compiler from the
ground up. Thus, entering our course, students are expected to have a general
understanding of the structure of a compiler and be especially comfortable
dealing with the abstract syntax. Familiarity with compilers from textbooks by
Wirth [38], Muchnick [28], and Appel [3, 4, 5] is assumed. Therefore, our
course omits these aspects and focuses on more in-depth semantic analysis,
type checking [32, §8–23], and runtime for lazy functional languages [18].

The course additionally assumes familiarity with some statically typed
programming languages. In particular, we assume students to be able to write
object-oriented code in C++ or Java, and be able to write functional code in
Haskell, OCaml, Scala, or a similar language.

The course load is approximately 15 hours per week. This includes two
lectures, two laboratories, and an estimated time for homework. In addition to
this course, students are enrolled in two other courses, which are also
organized in a block scheme.

###  4.2 Blocks

The course was organized into five blocks as the lecture topics and language
functionality became more complex. The Stella language evolves thoughout the
course from the core language, which is a simple functional language, to a
language with imperative objects [32, §18] or an ML-style language with
universal polymorphism [32, §23]. The organization of blocks was as follows:

#### Block 1. Simple Types

The first block covers the terminology and fundamental concepts necessary to
completely understand simply-typed lambda calculus and implement typechecking
for Stella Core, as well as some simple extensions from the _Syntactic Sugar
and Derived Forms_ , _Base Types_ , and _Simple Types_ categories.

The coding assignments in this block require students to implement:

  1. 1.

A typechecker for Stella Core, covering Nat, Bool, and function types.

  2. 2.

A typechecker for simple types: Unit, pairs, and sum types.

  3. 3.

For extra credit, students may implement a typechecker with support for some
of additional extensions: variants, tuples, records, let-bindings, letrec-
bindings, nested pattern matching (without exhaustiveness checks), type
aliasing, and general recursion.

A theoretical assignment is issued, focusing mainly on sum types and pattern
matching, making sure, students properly understand these concepts.

#### Block 2. Normalization and Recursive Types

The second block covers theoretical topics, discussing normalization
properties of simply typed lambda calculus [32, §12] and talking about
recursive types [32, §20]. No new assignments are issued in this block, since
students have an active assignment from the previous block.

#### Block 3. Imperative Objects

In the third block, we focus on adding imperative features like references
[32, §13] and exceptions [32, §14], and also discuss subtyping, aiming to
arrive at a language that supports imperative objects [32, §18]. We also
discuss Featherweight Java [17] and Welterweight Java [31]. The latter extends
Featherweight Java with imperative, stateful features, as well as thread-based
and lock-based concurrency. While Stella does not support nominal types,
students are still asked to complete theoretical excercises using Welterweight
Java.

The coding assignment in this block requires students to implement:

  1. 1.

A typechecker supporting sequencing, mutable references, unrecoverable errors,
and records with subtyping.

  2. 2.

For extra credit, students may implement a typechecker with support for some
of the additional extensions: subtyping for variants, exceptions with a fixed
(super)type, Top and Bot types, and exceptions with an open variant type.

#### Block 4. Type Reconstruction and Universal Types

The fourth block focuses on _type reconstruction_ [32, §22] (aka _type
inference_) and universal types [32, §23]. Additionally, we discuss Hindley-
Milder type system [16, 27] and the type inference algorithm for it [12].

The coding assignment in this block requires students to implement type
variables, universal types, and generic function declarations. The
implementation of the type checking here is complicated since students have to
take care with type variables bound by the forall quantifier in the
polymorphic types.

#### Block 5. Runtime for Lazy Functional Languages

This last block is dedicated to the exploration of runtime for lazy functional
languages. While this does not directly correspond to type checking, it helps
students appreciate sum types and variants more, as they see how they can be
efficiently implemented in a language like Haskell.

###  4.3 Assessment

Once a week at the start of the lecture, students complete a brief quiz
consisting of simple theoretical questions (typically, multiple-choice or
matching questions). The quiz is intended to be finished in the classroom
within 10 minutes and serves mostly as a tool to facilitate attendance and
wake students before the lecture.

To assess the students more comprehensively, three theoretical problem sets
are prepared and assigned as homework for one week each. In the labs, students
are working on their coding exercises and receive help from teaching
assistants. Most assignments have an extra credit part.

Students’ grades are computed based on completion of assignments and quizzes.
In case of late submissions or to allow for an improvement of their grade,
students are allowed to attend an oral exam to defend their implementation and
answer some more theoretical questions for some additional credit.

####  4.3.1 Solutions for Assignment 1

After completing the first coding assignment, we provide students with a
reference implementation in C++ and Java. In our course, these languages
turned out to be most popular among the students, but presented particular
implementation challenges. For instance, in C++, students struggled with the
complex handling of raw pointers and segfaults, partially due to raw pointers
in the generated code from BNFC. An additional motivation for sharing our
solution with the students was that the first assignment is the basis for all
subsequent assignments, and it is important that it has a good structure and
the ability to be easily extended. This allowed the students to compare and
refine their implementations or build entirely on ours. We find that without a
reference implementation for the first assignment, many students would waste
time rewriting the basic logic for each assignment, which is unacceptable
given the course’s time frame.

####  4.3.2 Collecting Student Submissions

For quizzes, we relied on the Moodle platform provided by Innopolis University
and automatically graded using it. Solutions to theoretical problem sets have
been also submitted through Moodle as PDF files, then graded manually.

For coding exercises, we considered using platforms such as
Codeforces101010https://codeforces.com/. Unfortunately, such platforms usually
deal with a single-module submissions, which cannot accommodate for the
complex compiler project structure.

Consequently, we redirected our focus to GitHub
Classroom111111https://classroom.github.com/ due to its advantages, including
the capability to create repositories in various programming languages as
templates for students to clone and commence their projects, as well as to
monitor student submissions by tracking commits. Although we chose GitHub
Classroom, it turned out not ideal for the following reasons:

  1. 1.

It is difficult to update the assignment template (e.g. fix problems, add
tests).

  2. 2.

It is impossible to offer templates in different languages.

  3. 3.

Consecutive assignments have separate repositories, it is impossible to submit
an individual commit as a solution to a particular assignment. To start a new
assignment, students had to clone the template each time and manually apply
their changes from the previous assignment.

In the end, taking into account the aforementioned issues, GitHub Classroom
has allowed us to keep track of students’ work throughout the course: tracking
their submission times, work completed, and assessments.

###  4.4 Results

The course was conducted for two groups with a total of 49 (active) students.
A final exam, which was optional and offered to all, was taken by
approximately 20% of the class. To provide students with the ability to obtain
additional guidance, make inquiries, and receive notifications, we provided a
Telegram chat room in addition to the Moodle and GitHub Classroom platforms
previously mentioned. Students completed their projects using various
programming languages.

Students selected different languages for their implementation. The
distribution of submissions by language is presented in Table 1. Students have
used C++ and Java extensively in the previous courses, so these were the
natural choices for most students. Kotlin was chosen by many students even
when they did not know the language before, due to simpler code structure. In
particular, while the Java template featured the Visitor pattern which many of
the students struggled with (despite being exposed to it in other courses), in
Kotlin students were able to use exhaustive pattern matching through when-
expressions, which they found very convenient when dealing with the nodes of
the abstract syntax tree.

Students had some freedom in selecting a subset of extensions to implement in
their submissions. In Table 2, we show for each feature, how many students
have implemented it fully (passing all tests) or partially. _Universal Types_
extension was not implemented correctly by many students due to the problem of
name captures, which is non-trivial to implement and also does not occur in
small test programs that students used for debugging. Many students who
attempted to implement _Stuctural Patterns_ struggled with handling contexts
properly. Often the reason was due to incorrect handling of mutable state in
an implementation of the Visitor pattern. When students approached the
implementation with a functional style, they were less likely to make
mistakes.

At the beginning of the course, we have encountered a major problem when
students were not able to work with the Makefile-based templates that we have
prepared originally. Setting up the environment and getting the project to a
point where they could begin writing code took one week, which has affected
the schedule of the course negatively, and forced us to skip some assignments.
Having learned from this experience, we plan to enhance IDE-friendly templates
for the future installation of the course.

Table 3 presents the distribution of the final grades for the course according
to different programming languages. With a relatively low number of students,
it is hard to draw any definitive conclusions from this data. It is perhaps
not so surprising to see many good grades for popular languages like Java,
Kotlin, and C++, since these languages had most support from the course team,
templates, and students were free to communicate and help each other in case
of technical difficulties. On the other hand, it is interesting to note that
students who selected languages that initially lacked templates for
implementation (Swift, Haskell, TypeScript) also achieved good grades. The
students who used these languages are relatively autonomous and proficient,
but we also believe that these languages possess features (such as pattern
matching) that noticeably simplify development of certain parts of a
typechecker, which might have helped these students as well.

Programming Language | Submissions
---|---
C++ | 17
Java | 12
Kotlin | 12
Python | 3
JavaScript | 2
Haskell | 1
Swift | 1
TypeScript | 1
Table 1: Language distribution. Feature | Full | Partial | Full, % | Partial, %
---|---|---|---|---
Core | 49 | 0 | 100% | 0%
Records | 46 | 0 | 94% | 0%
Pairs | 45 | 0 | 92% | 0%
Unit type | 44 | 0 | 90% | 0%
Sequencing | 43 | 0 | 88% | 0%
References | 42 | 0 | 86% | 0%
Sum types | 39 | 0 | 80% | 0%
Errors | 39 | 0 | 80% | 0%
Subtyping for records | 39 | 0 | 80% | 0%
Tuples | 38 | 3 | 78% | 6%
Universal types | 17 | 21 | 35% | 43%
Top and Bot types | 14 | 8 | 29% | 16%
Records | 12 | 5 | 24% | 10%
Exceptions with a fixed type | 11 | 0 | 22% | 0%
Exceptions with an open variant type | 10 | 0 | 20% | 0%
LetRec-binding | 9 | 0 | 18% | 0%
Subtyping for variants | 9 | 0 | 18% | 0%
Variants | 7 | 0 | 14% | 0%
Let-binding | 7 | 2 | 14% | 4%
Type aliases | 6 | 1 | 12% | 2%
Structural patterns | 3 | 21 | 6% | 43%
General recursion | 3 | 20 | 6% | 41%
Table 2: Implemented features in numbers. Language | A | A, % | B | B, % | C | C, % | D | D, %
---|---|---|---|---|---|---|---|---
C++ | 13 | 76% | 1 | 6% | 3 | 18% | 0 | 0%
Java | 12 | 75% | 2 | 17% | 0 | 0% | 1 | 8%
Kotlin | 8 | 67% | 4 | 33% | 0 | 0% | 0 | 0%
Python | 1 | 33% | 1 | 33% | 0 | 0% | 1 | 33%
JavaScript | 1 | 50% | 1 | 50% | 0 | 0% | 0 | 0%
Haskell | 0 | 0% | 1 | 100% | 0 | 0% | 0 | 0%
Swift | 1 | 100% | 0 | 0% | 0 | 0% | 0 | 0%
TypeScript | 0 | 0% | 1 | 100% | 0 | 0% | 0 | 0%
Table 3: Language to grades.

##  5 Conclusion and Future Work

We have presented a half-semester course that focuses on the study and
implementation of type systems, supported by a special programming language
Stella designed to facilitate students’ learning process. The language is
intended to accompany a well established textbook by Pierce [32], and our
preliminary experience shows that students that are used to C-like syntax
absorb the textbook material better when implementing Stella, at least
compared to implementing raw typed lambda calculi.

There are still many ways to improve Stella to better accommodate the needs of
the educational process. Nominal type systems prevail in modern programming
languages, so Stella should support them to enable a more fruitful discussion
and comparison with structural types. Bounded universal quantification is
currently not supported in Stella, but we plan to add it, since it allows for
a more direct experience with type systems that incorporate both parametric
polymorphism and subtyping, and is used a lot in languages like Java, Scala,
Kotlin, C#, OCaml. Annotating functions with the types of possible exceptions
is also currently not supported and provides for a relatively straightforward
but useful language extension. Row polymorphism [36] is a relatively rare but
important concept, that is currently not explored by Stella.

Although we focus mostly on type systems, we are also interested in
compilation techniques for functional programming languages. Stella’s
extension system may serve as a basis for studying different compiler
backends. In particular, while in our course we touch on STG [18], other
intermediate representations such as GRIN [9, 8] and HVM [25, 21] deserve
attention. However, more extensions related to operational semantics should be
considered for such an exploration. We feel that this belongs to a separate
course.

Another improvement to the course could be to improve the quality and
automation of tests. Instead of relying merely on the exit code of the type
checker, we should also take into account the type error message, which should
follow a standard specified in Stella documentation and available in the
playground. A partial implementation of that idea is given by error tags,
which are provided in Stella output. Additionally, in some situations, the
playground is able to suggest some alternative errors, allowing for some
variation in student’s implementations. An approach to automation of testing
similar to Lübke, Fuger, Bahnsen, Billerbeck, and Schupp [20] could also be
employed in the future.

Acknowledgements. We thank Artem Murashko, Timur Iakshigulov, Alexandr
Kudasov, Iskander Nafikov, and Danila Korneenko for their help with Swift, Go,
Rust, and Kotlin templates. We thank Asem Abdelhady for his contribution to
the test suite.

## References

  * [1]
  * [2] Alexander Aiken (1996): _Cool: A Portable Project for Teaching Compiler Construction_.  SIGPLAN Not. 31(7), p. 19–24, 10.1145/381841.381847.
  * [3] Andrew W. Appel (2004): _Modern Compiler Implementation in ML_.  Cambridge University Press, USA.
  * [4] Andrew W. Appel & Maia Ginsburg (2004): _Modern Compiler Implementation in C_.  Cambridge University Press, USA.
  * [5] Andrew W. Appel & Jens Palsberg (2003): _Modern Compiler Implementation in Java_ , 2nd edition.  Cambridge University Press, USA.
  * [6] Bill Appelbe (1979): _Teaching Compiler Development_.  In: Proceedings of the Tenth SIGCSE Technical Symposium on Computer Science Education, SIGCSE ’79, Association for Computing Machinery, New York, NY, USA, p. 23–27, 10.1145/800126.809546.
  * [7] Daniil Berezun & Dmitry Boulytchev (2022): _Reimplementing the Wheel: Teaching Compilers with a Small Self-Contained One_.  In Peter Achten & Elena Machkasova, editors: Proceedings Tenth and Eleventh International Workshop on Trends in Functional Programming In Education, TFPIE 2021 / 2022, Kraków, Poland (online), 16th February 2021 / 16th March 2022, EPTCS 363, pp. 22–43, 10.4204/EPTCS.363.2.
  * [8] Urban Boquist (1999): _Code optimization techniques for lazy functional languages_.  Ph.D. thesis, Chalmers Tekniska Högskola.
  * [9] Urban Boquist & Thomas Johnsson (1997): _The GRIN project: A highly optimising back end for lazy functional languages_.  In: Implementation of Functional Languages: 8th International Workshop, IFL’96 Bad Godesberg, Germany, September 16–18, 1996 Selected Papers 8, Springer, pp. 58–84, 10.1007/3-540-63237-9_19.
  * [10] Edwin Brady (2017): _Type-driven development with Idris_.  Simon and Schuster.
  * [11] Thierry Coquand & Gérard Huet (1988): _The calculus of constructions_.  Information and Computation 76(2), pp. 95–120, 10.1016/0890-5401(88)90005-3.
  * [12] Luís Damas (1984): _Type assignment in programming languages_.  Ph.D. thesis, University of Edinburgh, UK.  Available at https://hdl.handle.net/1842/13555.
  * [13] Moritz Eysholdt & Heiko Behrens (2010): _Xtext: implement your language faster than the quick and dirty way_.  In: Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, pp. 307–309, 10.1145/1869542.1869625.
  * [14] Markus Forsberg & Aarne Ranta (2004): _BNF Converter_.  In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell ’04, Association for Computing Machinery, New York, NY, USA, p. 94–95, 10.1145/1017472.1017475.
  * [15] Jean-Yves Girard (1986): _The system F of variable types, fifteen years later_.  Theoretical Computer Science 45, pp. 159–192, 10.1016/0304-3975(86)90044-7.
  * [16] R. Hindley (1969): _The Principal Type-Scheme of an Object in Combinatory Logic_.  Transactions of the American Mathematical Society 146, pp. 29–60, 10.1090/S0002-9947-1969-0253905-6.  Available at http://www.jstor.org/stable/1995158.
  * [17] Atsushi Igarashi, Benjamin C. Pierce & Philip Wadler (2001): _Featherweight Java: A Minimal Core Calculus for Java and GJ_.  ACM Trans. Program. Lang. Syst. 23(3), p. 396–450, 10.1145/503502.503505.
  * [18] Simon L. Peyton Jones (1992): _Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine_.  J. Funct. Program. 2(2), pp. 127–202, 10.1017/S0956796800000319.
  * [19] Neelakantan R. Krishnaswami (2009): _Focusing on pattern matching_.  In Zhong Shao & Benjamin C. Pierce, editors: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, ACM, pp. 366–378, 10.1145/1480881.1480927.
  * [20] Ole Lübke, Konrad Fuger, Fin Hendrik Bahnsen, Katrin Billerbeck & Sibylle Schupp (2023): _How to Derive an Electronic Functional Programming Exam from a Paper Exam with Proofs and Programming Tasks_.  In: Trends in Functional Programming in Education (TFPIE).
  * [21] Victor Maia (2023): _Higher-order Virtual Machine (HVM)_.  Available at https://github.com/HigherOrderCO/hvm.
  * [22] Luc Maranget (2007): _Warnings for pattern matching_.  Journal of Functional Programming 17(3), p. 387–421, 10.1017/S0956796807006223.
  * [23] Per Martin-Löf & Giovanni Sambin (1984): _Intuitionistic type theory_.  9, Bibliopolis Naples.
  * [24] Nicholas D. Matsakis & Felix S. Klock (2014): _The Rust Language_.  In: Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT ’14, Association for Computing Machinery, New York, NY, USA, p. 103–104, 10.1145/2663171.2663188.
  * [25] Damiano Mazza (2007): _A denotational semantics for the symmetric interaction combinators_.  Mathematical Structures in Computer Science 17(3), pp. 527–562, 10.1017/S0960129507006135.
  * [26] M. Mernik & V. Zumer (2003): _An educational tool for teaching compiler construction_.  IEEE Transactions on Education 46(1), pp. 61–68, 10.1109/TE.2002.808277.
  * [27] Robin Milner (1978): _A theory of type polymorphism in programming_.  Journal of Computer and System Sciences 17(3), pp. 348–375, 10.1016/0022-0000(78)90014-4.
  * [28] Steven S. Muchnick (1998): _Advanced Compiler Design and Implementation_.  Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.
  * [29] Victor Nazarov, Hamish Mackenzie & Luite Stegeman (2015): _GHCJS Haskell to JavaScript compiler_.  Available at https://github.com/ghcjs/ghcjs.
  * [30] Francisco Ortin, Daniel Zapico & Juan Manuel Cueva (2007): _Design Patterns for Teaching Type Checking in a Compiler Construction Course_.  IEEE Transactions on Education 50(3), pp. 273–283, 10.1109/TE.2007.901983.
  * [31] Johan Östlund & Tobias Wrigstad (2010): _Welterweight Java_.  In: Proceedings of the 48th International Conference on Objects, Models, Components, Patterns, TOOLS’10, Springer-Verlag, Berlin, Heidelberg, p. 97–116, 10.1007/978-3-642-13953-6_6.
  * [32] Benjamin C. Pierce (2002): _Types and programming languages_.  MIT Press.
  * [33] Gordon D. Plotkin (1977): _LCF Considered as a Programming Language_.  Theor. Comput. Sci. 5, pp. 223–255, 10.1016/0304-3975(77)90044-5.  Available at https://api.semanticscholar.org/CorpusID:53785015.
  * [34] John C Reynolds (1974): _Towards a theory of type structure_.  In: Programming Symposium: Proceedings, Colloque sur la Programmation Paris, April 9–11, 1974, Springer, pp. 408–425, 10.1007/3-540-06859-7_148.
  * [35] Peter Sestoft (1996): _ML Pattern Match Compilation and Partial Evaluation_.  In Olivier Danvy, Robert Glück & Peter Thiemann, editors: Partial Evaluation, International Seminar, Dagstuhl Castle, Germany, February 12-16, 1996, Selected Papers, Lecture Notes in Computer Science 1110, Springer, pp. 446–464, 10.1007/3-540-61580-6_22.
  * [36] M. Wand (1989): _Type inference for record concatenation and multiple inheritance_.  In: [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp. 92–97, 10.1109/LICS.1989.39162.
  * [37] Richard Wei, Dan Zheng, Marc Rasi & Bart Chrzaszcz (2023): _Differentiable Programming Manifesto_.  Available at https://github.com/apple/swift/blob/main/docs/DifferentiableProgramming.md.
  * [38] Niklaus Wirth (1996): _Compiler Construction_.  Addison Wesley Longman Publishing Co., Inc., USA.
  * [39] Brent A. Yorgey (2023): _Disco: A Functional Programming Language for Discrete Mathematics_.  Electronic Proceedings in Theoretical Computer Science 382, p. 64–81, 10.4204/eptcs.382.4.