5eqn

PLT

题解(12)

/ 注册

全部文章 / PLT （共1篇）

DTmpl: 基于依值类型和模板的高级语言代码生成思路

模板是针对高级语言代码生成的一种已有方案之一，工业上的例子包括 ANTLR 等。依值类型被广泛用于证明验证或自动证明，例子包括 Agda 等。然而目前来看模板的自由度极低，应对一些需要展开的任务，例如生成 Golang 代码中的大量错误处理，实现起来比较困难。依值类型虽然允许直接通过搜索生成想要的程...

Idris2 Go

2023-07-15

0 317