我理想中的编程语言

2025.1.8 注

这是当时我对「理想编程语言」这个大问题的一点思考，后续在尝试实现的时候遇到了难以逾越的问题，说明我当时把问题想简单了。

正文

前面看了很多 Idris2 的内容，就是在给这篇陈述铺垫。我在 4 月末到 5 月末几乎一直在写 Aevum 这门语言的词法分析、语法分析和语义分析，虽然没有涉及代码生成，但光是类型检查已经很困难了。最终 384 行的程序，虽然没有用依值类型来给类型检查的正确性添加证明，但已经足够简洁、清晰、有效。但对于下一阶段的代码生成，我需要先回答一些问题来确定编码方向：我要把 Aevum 的语法树编译成什么语言？只允许编译成 LLVM，还是允许用户对各类主流语言进行建模，然后直接输出目标语言？如何处理对线性资源和不确定性的建模？如何处理好 Monad 和 Linear Types 的关系？在对 Idris2 的 QTT 进行初步学习后，我对这些问题也形成了初步的答案。

好的语言应该是函数式的

人的思维方式是非常函数式的。例如如果让你思考如何交换两个内存地址的数据，假如你从未学过编程，同时浅显地把「内存地址」理解成常识意义上的「地址」，你首先想到的大概率是「两坨数据直接互相交换位置」的场景。但经过 C 语言的洗脑后，你所想到的就变成了「开一个临时地址，把前一个数据放到临时地址，后一个放到前一个的位置，临时地址的数据放到后一个的位置」。这是违反直觉的。从起因直接「映射」到结果，才是更符合人类直觉的思维方式。

函数式语言被人诟病在于不能良好地对内存进行建模，且依赖「自函子范畴的幺半群」（Monad）之类的神秘概念对逻辑进行精简，因此通常被认为是更不符合人类直觉的那一方。但我认为在利用依值类型和线性类型对常用的「外部资源」，例如内存、输入输出（IO）、数据库等建模后，函数式语言比面向过程、面向对象的语言更符合人类直觉，这也是为什么我曾说 C 系语言（包括 C, C++, C#, Java, JS, Python, Rust…）都是对人类思维的绑架。至于具体如何建模，我后面会给出例子。

值得一提的是，Rust 里面用到了 Affine Types，除了允许凭空 free 掉一个变量，和 Linear Types 并没有不同（Linear Types 就是一个线性变量在一个函数中一定被使用正好一次）。同时 Rust 里面有大量函数式语言里的特性，例如模式匹配（高级 switch case）。这也是为什么在所有 C 系语言中，我最欣赏的语言是 Rust.

大部分语言（C#, Java, Python…）都会使用一种叫「垃圾回收」的机制（GC），简而言之就是不像 C 里面一样 malloc 了什么都要 free，有了 GC 之后你只管 malloc 就行，malloc 出来的东西会被「引用计数」，程序定期检查哪些变量没被引用，然后把这些内存批量回收。和 Rust 的不同在于，Rust 相当于通过所有权和生命周期之类的机制，自动算出来哪里需要调用 free. 我认为 GC 这种机制虽然降低了认知压力，但我不认为这些语言使用 GC 能给其带来优越性，理由有三点：

首先这种机制不能让你逃避对引用变量（你在一个函数里修改了这个值，出了函数之后你的改动还留着，类似于 C 里面的指针指向的变量）和值变量（你在函数里只能修改它的「拷贝」，出了函数之后值还是原来的，类似于 C 里面的无指针结构体）的区分，因此你还是要对内存进行建模，而你凭借直觉产生的建模方式应该和 Rust 的建模方式差不了多少（新人学习 Rust 容易把所有权、生命周期这些玩意当作 brand new 的概念来学，就像学习课内知识一样，但这是被 Matrix 使用学分绩荼毒了学习观导致的，实际上这些只是人类直觉的一部分），GC 不逼迫你写出对内存的建模反而容易让人在不熟悉语言的内存分配机制的情况下产生错误的假设，且不能像在 Rust 里一样得到编译器提醒。

其次在函数式语言中，修改对内存的建模方式理论上就能实现 GC，而其建模方式不像 Rust 和语言直接绑定，在函数式语言中可以利用 Linear Types 等类型机制手动拼出来，其对应的编译器后端也可以开放修改接口，允许用户实现对语言的高度自定义。

最后 GC 在我看来很没素质，GC 直接导致语言的实际运行流程和看代码得出的运行流程不同，虽然在工程意义上没什么影响，但由于我是一个高度感性的人，我就认为 GC 很没素质。

好的语言要能对其他语言建模

一个语言若要被「应用」，必须要有匹配的生态。例如 Golang 中有完善的 ORM，可以用简洁的 Golang 代码去操作各类数据库，ORM 可以帮忙生成 SQL 语句。JS / TS 本身作为浏览器使用的默认脚本语言，也有 React、Vue 等前端框架，在这些前端框架的基础上还有大量的组件库。这些生态如果要全靠自己组建，是相当不现实的。但如果直接写这些语言的代码，难免有一种搬砖感，因为要处理大量的重复逻辑，尤其是在客户端和服务端语言不同的时候。理想状况下，我们应该有一套对这些语言建模的方法，把高阶的逻辑转化成这些具体的语言。

我的设想

以一个简单的 CRUD （增删改查）服务器为例，接受 HTTP 协议的增删改查请求，给出回复并和数据库对接。如果用 Golang 写内容将相当多，这里首先用我计划完成的 Aevum 语言写出逻辑框架，然后展示如何对语言本身建模。

data HTTPMode = Create | Read | Update | Delete

-- Other type definitions...

run : IO 0 -> IO 1 & Server addr
run io@void -> let srv = newServer addr in ++io@"Server listening on {addr}" & srv@[]

register : m : HTTPMode -> Server addr -> Server addr
register m srv@ls = let ls' = handle m :: ls in srv@ls'

create : HTTP Create 0 & DB Data New 0 -> HTTP Create 1 & DB Data New 1
create io@req & db@id = ++io@id & ++db@req.dat

read : io@req : HTTP Read 0 & DB Data req.id -> HTTP Read 1 & DB Data req.id
read io@req & db@dat = ++io@dat & db@dat

update : io@req : HTTP Update 0 & DB Data req.id -> HTTP Update 1 & DB Data req.id
update io@req & db@dat = ++io@dat & db@req.dat

delete : io@req : HTTP Delete 0 & DB Data req.id -> HTTP Delete 1 & DB Data req.id
delete io@req & db@dat = ++io@dat & db@void

以 update 函数为例，输入 req 中包含编号 id 和数据 dat，同时初始状态下数据库 db 在 req.id 的位置下是旧数据 dat. 这个程序直接指定 update 结束后，返回的数据是旧数据 dat，数据库 db 在 req.id 的位置下是请求中的新数据 req.dat，只描述了一个映射关系而不是传值的过程。这种描述方式是高度符合人类直觉的。

注意这里形如 io 的 Linear Token 和类型都能表示形如 req 的数据的「位置」，但在人类直觉中，Linear Token 表示的部分处在空间上不可重合的维度，类型则处在可以重合的维度。对于 Linear Token，写在类型签名里面没有意义，因为在运算的每个过程都要去追踪，每个值都要带上 Token，因此在类型签名里面再写就重复了。对于类型，写在值旁边没有意义，因为每个值不能变化类型（注意 Linear Token 则可以变化），其类型可以被编译器推断出来。这些因素叠加，就导致了虽然它们同为「位置」信息，但写在截然不同的地方的结果。

对于建模其他语言，我可能需要了解更多编译原理再来仔细思考……

我想到一种「代码嵌入」的形式：

newServer : addr : Addr -> Server addr
newServer addr = let srv = go#"gin.Default()" in srv@[]

但可能效果不好，理想状况下应该是给编译器开出一个可编程代码生成模块，在里面对其他语言进行建模。