Type-Theory as a Language Workbench

Language Workbenches offer language designers an expressive environment in which to create their Domain Specific Languages (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 Intermediate Representations (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, our paper describes our design choices for well-typed IR design that includes support for well-typed holes, how common sub-expression elimination is achieved in a well-typed setting, and how the mechanised type-soundness proof for Velo is the source of the evaluator. This artefact presents our implementation of Velo (as realised in Idris2), and the test suite used