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.
翻译：语言工作箱为语言设计者提供一种表达式环境来创建自己的 DSL 。 同样, 对机械化元理论的研究也表明, 以打字方式打字的语言如何提供表达式环境来正式化和研究 DSL 及其元理论特性。 但我们能否宣称, 以打字方式打字的语言有资格成为语言工作箱? 我们主张是的! 我们已经开发了一个名为 Velo 的 Expempil DSL 的演示性文件, 它不仅展示了以打字方式打字的识别和操作 IR 技术, 而且还以打字方式打字的语言做了精细的语言工作。 Velo 是一种简单的经核实的语言, 并带有一个完整的编译器管道: parser、 elaborator、 REPL、 评审员和编译员。 具体地说, 我们描述我们用于精准型 IR 设计的设计选择, 包括支持精准型的洞洞, 如何在类型良好的环境中实现 CSE,, 如何使Velo 的机械型类型健康证明是评价者的来源 。
相关内容
微信扫码咨询专知VIP会员