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

模板是针对高级语言代码生成的一种已有方案之一，工业上的例子包括 ANTLR 等。依值类型被广泛用于证明验证或自动证明，例子包括 Agda 等。然而目前来看模板的自由度极低，应对一些需要展开的任务，例如生成 Golang 代码中的大量错误处理，实现起来比较困难。依值类型虽然允许直接通过搜索生成想要的程序，但其目前在工业界的用例 F* 和 Idris2 都没有和现有语言、现有生态结合的能力，自身没有也难以形成良好的生态。

为综合两方的优势，我提供一种名为 DTmpl 的高级语言代码生成实现思路。DTmpl 取「依值类型」的首字母缩写 DT 和「模板」的缩写 Tmpl 组合而成。不过注意这个是「思路」，换言之还有一些问题没有解决。

假设读者对 Monad 和依值类型有基础的认识。

从实际例子开始

以下是一个基于 Golang Gin 和 GORM 框架的后端服务例子，注意这只是一个非常简单的的 Update 服务：

func SetBPM(db *gorm.DB) gin.HandlerFunc {
	return func(c *gin.Context) {
		// Get the song ID from the request parameters
		id := c.Param("id")

		// Read the song from the database
		var song Song
		if err := db.First(&song, id).Error; err != nil {
			rep := &GeneralReply{
				Success: false,
				Msg:     fmt.Sprintf("failed to read song: %v", err),
			}
			c.JSON(http.StatusInternalServerError, rep)
			return
		}

		// Parse the BPM and offset values from the request body
		var requestBody struct {
			BPM    float64 `json:"bpm"`
			Offset float64 `json:"offset"`
		}
		if err := c.ShouldBindJSON(&requestBody); err != nil {
			rep := &GeneralReply{
				Success: false,
				Msg:     fmt.Sprintf("failed to parse request body: %v", err),
			}
			c.JSON(http.StatusBadRequest, rep)
			return
		}

		// Update the song's BPM and offset
		song.BPM = requestBody.BPM
		song.Offset = requestBody.Offset

		// Save the updated song to the database
		if err := db.Save(&song).Error; err != nil {
			rep := &GeneralReply{
				Success: false,
				Msg:     fmt.Sprintf("failed to save updated song: %v", err),
			}
			c.JSON(http.StatusInternalServerError, rep)
			return
		}

		// Reply with a success message
		rep := &GeneralReply{
			Success: true,
			Msg:     "BPM and offset successfully updated.",
		}
		c.JSON(http.StatusOK, rep)
	}
}

我们尝试用某种伪码理一下核心逻辑，其中 <- 记号参考 Monad 的规范，表示经过一些处理后赋值；-> 表示箭头类型，是一个类型构造器；=> 是匿名函数构造器，省略了前面的 \ 符号，不再像 Idris2 中表达隐式参数，我选择使用花括号表达隐式参数：

DB : Type
Ctx : Type

f = db : 1 DB =>
    ctx : 1 Ctx =>
    cont : 1 DB -> 1 Ctx -> Any =>
    ctx, id <- /* get param from ctx */
    db, song </* process error */- /* get from db */
    ctx, req </* process error */- /* bind from ctx */
    song <- /* copy from req to song */
    db </* process error */- /* save song to db */
    cont db c

结合 Monad

在正常的 Monad 模式中，如果出现形如 a <- b 的语句，往往有类似于 a : A, b : M A 的类型关系。于是我设想一种推广，只要程序中出现 (a : A) <- (b : (B -> Any) -> Any) 形式的语句时，编译时尝试搜索到一个 f : B -> (A -> Any) -> Any 的函数，并尝试以此耦合 b 和后续的语句（如果你愿意做点习题的话，考虑证明这个耦合是可能的，习题答案在文末给出）。这样，我们通过规定右侧函数的返回类别和推断左侧参数类别，就可以实现自动织入错误处理等程序：

DB : Type
Ctx : Type
Song : Type
Req : Type
E : Type -> Type

getParam : 1 Ctx -> (1 Ctx -> String -> Any) -> Any
getSong : 1 DB -> (1 E DB -> Song -> Any) -> Any
bind : 1 Ctx -> (1 E Ctx -> Req -> Any) -> Any
copy : Req -> Song -> (Song -> Any) -> Any
saveSong : 1 DB -> Song -> (1 E DB -> Any) -> Any
handleErr : {T : Type} -> 1 E T -> (T -> Any) -> Any

f = db : 1 DB =>
    ctx : 1 Ctx =>
    cont : 1 DB -> 1 Ctx -> Any =>
    ctx, id <- getParam ctx
    db, song <- getSong db
    ctx, req <- bind ctx
    song <- copy req song
    db <- saveSong db song
    cont db c

线性类型

可以看到代码中有一些类型被标注了 1, 这表示其如果出现在语境中，必须被使用恰好一次。使用意味着将其作为返回值，调用之，或者将其作为一个线性参数，也就是另一个输入类型对应位置标了 1 的函数。作为返回值例如：

f = a : 1 A => a

调用例如：

f = p : 1 (A -> B) => a : A => p a

作为线性参数例如：

f = a : 1 A => a
g = a : 1 A => f a

作为习题，请找出以下代码中的错误，习题的答案将在文末给出： （注：该习题可能有事实性错误，我近期发现我对线性类型的理解有些偏差）

f = p : 1 (A -> B) => a : 1 A => p a

模板

众所周知，函数式语言很容易转换成非函数式语言，只需要目标语言支持匿名函数基本就没问题。顺着这种思路，我们不妨假设我们不需要处理构造出匿名函数的框架（包括形成和施加参数），框架的生成规则硬编码在编译器里面，我们只需要构造出其内容。

由于部分语言里面没有泛型，大部分语言里面没有依值类型，但依值类型实际上只影响了类型检查，所以如果只考虑编译到目标语言的话，我们直接把类型的参数塞到名字里面就可以了，把需要用到的信息存进结构体里面或者硬编码判断。不过结构体的处理较为繁琐，在这一小节暂不讨论。事实上类型这里也有对应的类型匿名函数的框架，但这个框架的处理是平凡的。

同时，考虑到一个函数编译成的最终文本实质上只和其形参名有关，而形参名是可以随意指定的，因此我们不妨将最终文本视为一个函数，这实质上就是模板，而模板变量名取决于形参名。

这样，我们可以为上述程序加入模板的内容，暂时不想管 Any 所以全部写成了 Void：

DB : Type
DB = `*gorm.DB`

Ctx : Type
Ctx = `*gin.Context`

Song : Type
Song = `Song`

Req : Type
Req = `Req`

E : Type
E = `error`

getParam = ctx : 1 Ctx =>
           db : 1 DB =>
           cont : 1 (1 Ctx -> 1 DB -> String -> Void) => 
           cont ctx db ``ctx`.Param("id")`

getSong = ctx : 1 Ctx =>
          db : 1 DB =>
          cont : 1 (1 E -> 1 Ctx -> 1 DB -> Song -> Void) => 
         `var song `Song``
         `err := `E DB`{Val: `db`, Err: `db`.First(&song, id).Error}`
          cont `err` ctx db `song`

bind = ctx : 1 Ctx =>
       db : 1 DB =>
       cont : 1 (1 E -> 1 Ctx -> DB -> Req -> Void) =>
      `var req `Req``
      `err := `E Ctx`{Val: `ctx`, Err: `ctx`.ShouldBindJSON(&req)}`
       cont `err` ctx db `req`

copy = ctx : 1 Ctx =>
       db : 1 DB =>
       req : Req =>
       song : Song =>
       cont : 1 (1 Ctx -> 1 DB -> Song -> Void) =>
      ``song`.BPM = `req`.BPM`
      ``song`.Offset = `req`.Offset`
       cont ctx db song

saveSong = ctx : 1 Ctx =>
           db : 1 DB =>
           song : Song =>
           cont : 1 (1 E -> 1 Ctx -> 1 DB -> Void) =>
          `err := `E DB`{Val: `db`, Err: `db`.Save(&`song`).Error}`
           cont `err` ctx db
           
handleErr = e : 1 E =>
            ctx : 1 Ctx =>
            db : 1 DB =>
            cont : 1 Void =>
            next : 1 Ctx -> 1 DB -> 1 Void -> Void =>
            if ``e.Err` != nil`
                abort ctx db cont
            else
                next ctx db cont
            
abort = ctx : 1 Ctx =>
        db : 1 DB =>
        cont : 1 Void =>
       `rep := &gin.H{`
       `    "success": false,`
       `    "msg":     "unknown error",`
       `}`
       ``ctx`.JSON(http.StatusInternalServerError, rep)`
        cont
        
commit = ctx : 1 Ctx =>
         db : 1 DB =>
         cont : 1 Void =>
        `rep := &gin.H{`
        `    "success": true,`
        `    "msg":     "unknown no error",`
        `}`
        ``ctx`.JSON(http.StatusOK, rep)`
         cont

f = db : 1 DB =>
    ctx : 1 Ctx =>
    cont : 1 Void =>
    ctx, db, id <- getParam ctx db
    ctx, db, song <- getSong ctx db
    ctx, db, req <- bind ctx db
    ctx, db, song <- copy ctx db req song
    ctx, db <- saveSong ctx db song
    commit ctx db cont

吐槽一下 Golang 允许返回 tuple, 却不允许函数参数接受 tuple, 导致要么使用 CPS 并把 Monad 扩展成线性的，要么需要有一个函数返回 tuple 但在 monad bind 的时候拆成分立单元的机制。上面的写法使用了 CPS, 对不熟悉的人而言可能看着会晕（我也有可能有些地方写错了……），但我觉得更对称一些。下面我用第二种写法写一次：

DB : Type
DB = `*gorm.DB`

Ctx : Type
Ctx = `*gin.Context`

Song : Type
Song = `Song`

Req : Type
Req = `Req`

E : Type
E = `error`

getParam = ctx : 1 Ctx =>
           db : 1 DB =>
           ctx, db, ``ctx`.Param("id")`

getSong = ctx : 1 Ctx =>
          db : 1 DB =>
         `var song `Song``
         `err := `E DB`{Val: `db`, Err: `db`.First(&song, id).Error}`
          `err`, ctx, db, `song`

bind = ctx : 1 Ctx =>
       db : 1 DB =>
      `var req `Req``
      `err := `E Ctx`{Val: `ctx`, Err: `ctx`.ShouldBindJSON(&req)}`
       `err`, ctx, db, `req`

copy = ctx : 1 Ctx =>
       db : 1 DB =>
       req : Req =>
       song : Song =>
      ``song`.BPM = `req`.BPM`
      ``song`.Offset = `req`.Offset`
       ctx, db, song

saveSong = ctx : 1 Ctx =>
           db : 1 DB =>
           song : Song =>
          `err := `E DB`{Val: `db`, Err: `db`.Save(&`song`).Error}`
           `err`, ctx, db
           
handleErr = e : 1 E =>
            ctx : 1 Ctx =>
            db : 1 DB =>
            next : 1 Ctx -> 1 DB -> Any =>
            if ``e.Err` != nil`
                abort ctx db
            else
                next ctx db
            
abort = ctx : 1 Ctx =>
        db : 1 DB =>
       `rep := &gin.H{`
       `    "success": false,`
       `    "msg":     "unknown error",`
       `}`
       ``ctx`.JSON(http.StatusInternalServerError, rep)`
        
commit = ctx : 1 Ctx =>
         db : 1 DB =>
        `rep := &gin.H{`
        `    "success": true,`
        `    "msg":     "unknown no error",`
        `}`
        ``ctx`.JSON(http.StatusOK, rep)`

f = db : 1 DB =>
    ctx : 1 Ctx =>
    cont : 1 Any =>
    ctx, db, id <- getParam ctx db
    ctx, db, song <- getSong ctx db
    ctx, db, req <- bind ctx db
    ctx, db, song <- copy ctx db req song
    ctx, db <- saveSong ctx db song
    commit ctx db

立省 10 行。从兼顾效率和对称性的角度讲，我认为采用「写作返回 tuple, 读作线性 CPS」比较合适，但这样真的要实现编译器的时候会有些眩晕。

可以看到有非常多重复且无用的线性变量重新赋值，但考虑到 <- 如果没有被织入其他逻辑（例如错误处理）的话，实际上是线性的，因此考虑隐去一些参数，只在织入逻辑的时候要求把参数填满：

DB : Type
DB = `*gorm.DB`

Ctx : Type
Ctx = `*gin.Context`

Song : Type
Song = `Song`

Req : Type
Req = `Req`

E : Type
E = `error`

getParam = ctx : 1 Ctx =>
           ctx, ``ctx`.Param("id")`

getSong = db : 1 DB =>
         `var song `Song``
         `err := `E DB`{Val: `db`, Err: `db`.First(&song, id).Error}`
          `err`, db, `song`

bind = ctx : 1 Ctx =>
      `var req `Req``
      `err := `E Ctx`{Val: `ctx`, Err: `ctx`.ShouldBindJSON(&req)}`
       `err`, ctx, `req`

copy = req : Req =>
       song : Song =>
      ``song`.BPM = `req`.BPM`
      ``song`.Offset = `req`.Offset`
       song

saveSong = db : 1 DB =>
           song : Song =>
          `err := `E DB`{Val: `db`, Err: `db`.Save(&`song`).Error}`
           `err`, db
           
handleErr = e : 1 E =>
            ctx : 1 Ctx =>
            db : 1 DB =>
            next : 1 Ctx -> 1 DB -> Any =>
            if ``e.Err` != nil`
                abort ctx db
            else
                next ctx db
            
abort = ctx : 1 Ctx =>
        db : 1 DB =>
       `rep := &gin.H{`
       `    "success": false,`
       `    "msg":     "unknown error",`
       `}`
       ``ctx`.JSON(http.StatusInternalServerError, rep)`
        
commit = ctx : 1 Ctx =>
         db : 1 DB =>
        `rep := &gin.H{`
        `    "success": true,`
        `    "msg":     "unknown no error",`
        `}`
        ``ctx`.JSON(http.StatusOK, rep)`

f = db : 1 DB =>
    ctx : 1 Ctx =>
    cont : 1 Any =>
    ctx, id <- getParam ctx
    db, song <- getSong db
    ctx, req <- bind ctx
    song <- copy req song
    db <- saveSong db song
    commit ctx db

现在的代码看起来清晰不少，且核心逻辑集中在 f, 可以看到相比原版 Golang 代码非常短小。如果这种技术被应用于工业，在阅读源码的时候能比 Golang 中更快地把握核心逻辑，同时还附带了免费的线性检查和依值类型的表达力，但代价是总的代码量变多了……等等，这真的是代价吗？

复用

这一段可能稍微带点幻想成分。目前而言我们提炼出来的东西很难复用，但考虑到依值类型语言的表达力，我们为什么不能把 project-specific 的部分全部抽出来作为参数，包装成某种「我对 Golang 的认识以依值类型程序存储」的可复用形式呢？即使是对于纯 Golang 开发，如果有较多的重复开发工作，这种方式可以允许我们对于任何一处感觉「逻辑很简单但代码一大块」的东西，都可以以非常快速且安全地实现。在重复开发足够多的时候，甚至可以只写核心的 f 函数，可以想象相比直接硬搓 Golang 代码，这将节约多少时间！即使相比面向 ChatGPT 编程，我们这种思路都相当有竞争力，因为这种依值类型语言无论从表达精炼度、精确度和安全性考虑，都远超自然语言。这也是为什么我并不看好某些人认为是「未来」的自然语言编程，把需求用自然语言表述出来的那一刻已经输了。

应该用自然语言表述的不是需求，而是把一群人聚在一起的图景。

解耦

软件工程中一直有对「逻辑和框架解耦」的追求，我也为此做过诸多尝试，但过往的尝试大多局限于把每个具体的需求拆成两层以隔离逻辑和框架，起到的复用作用很小，且解耦之后也不会有换框架的需求，有「过度优化」之嫌。但现在这个思路由于表达力较强，不仅能实现非常高程度的复用，而且可以很方便地写多个语言的对接代码，实现真正的「逻辑和框架解耦」！代价就是需要经过一次代码生成，不过有了代码生成，这个方式甚至能做到「语言无关」，生成绝大多数语言的代码，可以当作是不仅和框架解耦，和语言也实现了解耦！

待解决的问题

虽然这种思路看起来前景很广阔，但可能也将是一次失败的尝试。目前来看，有很多关键的问题没有解决，例如：

1. 结构体怎么表示？Golang 是接受匿名结构体的，但并不是所有语言都这样，这本质上要求我们有在公共语境塞东西的能力，我们的模板就要为这一点专门提供支持。有两种方式，一种是在模板里面标注用于创建具体字段的部分只会在公共语境中被一次性声明，这样虽然结构体本身里面东西很多，但不会每次出现都带上全部的内容；另一种是直接开一个公共的地方强行塞一些代码进去。但第一种方式的缺点是对公共部分进行特判的部分容易发展成雪山，第二种方式的缺点是要么需要把逻辑写在不同的地方，要么就会出现类型定义区里面私有和公共代码交互的奇观，哪一种都不是我们希望发生的。
2. 以目前 CPS 的思路，生成的目标代码中会有大量匿名函数的嵌套调用，在目标语言中可能会造成严重的性能问题，因此需要一种内联函数的手段。但由于目标语言中也可能需要有匿名函数，因此我们需要一种选择而内联与否的手段，但这一选择增加了编码的复杂性。有没有更美丽的方案？我的一种设想是根据函数在源语言的实际调用情况决定内联与否，只不内联单独作为参数的函数，这样就避免了主动选择。但由于内联函数和非内联函数在目标语言的写法往往不一样，写函数的时候还是需要预先确定内联还是不内联，后续如果要修改的话就要切换不同的写法。要避免这一缺陷，我们需要对内联转换为非内联的语法（反过来也可以）进行建模，但考虑到 Golang 有允许函数返回 tuple 但不接受 tuple 类型参数的特性，对于 Golang 我们要么在函数调用的语法中预先添加一个赋值语句接受 tuple, 要么用 CPS, 但无论哪种的实现都不简单。
3. 依值类型拥有很逆天的自由度，涉及依值类型的结构体该如何表达？
4. 模式匹配如何处理？
5. 如何利用立方类型论实现逻辑和算法的解耦？

类似这样的问题还有很多，受篇幅所限，我就不一一详述了。但这个方向我个人认为值得一试。

习题答案

习题一

只要程序中出现 (a : A) <- (f : (B -> Any) -> Any) 形式的语句（为了证明方便，我相对原题重命名了一下）时，编译时尝试搜索到一个 bind : B -> (A -> Any) -> Any 的函数，并尝试以此耦合 b 和后续的语句。考虑证明这个耦合是可能的。

注意前面的 (a : A) 实际上是一个函数的形参，假设这个函数是 cont, 它返回类型 C 的实例，那么我们语境中有的东西包括：

f : (B -> Any) -> Any
bind : B -> (A -> Any) -> Any
cont : A -> C

现在我们需要构造出 C. 考虑如下构造：

c : C
c = f {Any = C} (b : B => bind {Any = C} b cont)

事实上我给出的示例代码中用到的是这条的推广版，不过我只是直觉感觉其可以推广，真的要写出来的话涉及一些比较繁琐的细节，故懒得写了。

习题二

请找出以下代码中的错误：

f = p : 1 (A -> B) => a : 1 A => p a

回想起通过调用实现使用的例子：

f = p : 1 (A -> B) => a : A => p a

唯一的区别是习题中的 A 是线性的。容易发现，这个 A 被作为 p 的参数，但 p 里面 A 却不是线性参数，因此过不了线性检查。如果要保持 A 参数的线性，正确的版本应该是：

f = p : 1 (1 A -> B) => a : 1 A => p a

在处理线性类型的时候，一个重难点就是对 1 A -> B, 1 (A -> B) 和 1 (1 A -> B) 的区分。如果你做了这道题目，应当能加深理解。我之前看 Idris2 的 Linear Types 应用的论文时深受此困扰。