A modular, algebra-sequenced paramorphic constraint-based type checker for Rosetta

Snyder, Mark H.

Publication

A modular, algebra-sequenced paramorphic constraint-based type checker for Rosetta

Snyder, Mark H.

Abstract

The objective of this thesis is to demonstrate the feasibility of performing static analysis, specifically type checking, in a particularly modular way. We use a term space of fixpoints of sums of functors so that, by writing individual type checkers for each portion of the entire language, we can then combine those algebras into an algebra that functions over the entire target language. The overall computational style employed uses a sequenced paramorphism to reduce the terms to the value space of types. As a proof of concept, this thesis presents a nominal typechecker in Haskell for the language Rosetta. It relies heavily on InterpreterLib, a Haskell library for designing interpreters in exactly the style described.