License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.EVCS.2023.9
URN: urn:nbn:de:0030-drops-177797
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17779/
Go to the corresponding OASIcs Volume Portal

de Muijnck-Hughes, Jan ; Allais, Guillaume ; Brady, Edwin

Type Theory as a Language Workbench

pdf-format:
OASIcs-EVCS-2023-9.pdf (0.6 MB)

Abstract

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 Vélo that showcases not only dependently typed techniques to realise and manipulate Intermediate Representations (IRs), but that dependently typed languages make fine language workbenches. Vélo 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 IR 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 Vélo is the source of the evaluator.

BibTeX - Entry

@InProceedings{demuijnckhughes_et_al:OASIcs.EVCS.2023.9,
  author =	{de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin},
  title =	{{Type Theory as a Language Workbench}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{9:1--9:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17779},
  URN =		{urn:nbn:de:0030-drops-177797},
  doi =		{10.4230/OASIcs.EVCS.2023.9},
  annote =	{Keywords: dependent types, language workbenches, idris2, dsl, edsl, intrinsically scoped, well typed, co-De Bruijn}
}

Keywords: dependent types, language workbenches, idris2, dsl, edsl, intrinsically scoped, well typed, co-De Bruijn
Collection: Eelco Visser Commemorative Symposium (EVCS 2023)
Issue Date: 2023
Date of publication: 21.03.2023
Supplementary Material: We have made Vélo’s source available both as a reproducible artifact and freely available source code:
Software (Source Code): https://github.com/jfdm/velo-lang
Software (Artifact): https://doi.org/10.5281/zenodo.7573031

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI