Type Theory as a Language Workbench

TL;DR

This paper demonstrates that dependently typed languages can serve as effective language workbenches by developing Velo, a verified DSL with a complete compiler pipeline and mechanised meta-theory.

Contribution

It introduces Velo, a dependently typed DSL that functions as a language workbench, showcasing formal IR design, type-soundness, and a full compiler pipeline.

Findings

Velo supports well-typed holes and IR manipulation.

CSE is achieved within a well-typed framework.

Mechanised proof of type soundness underpins the evaluator.

Abstract

Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have developed an exemplar DSL called Velo that showcases not only dependently typed techniques to realise and manipulate IRs, but that dependently typed languages make fine language workbenches. Velo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IRs design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Velo is the source of the evaluator.