为什么静态语言会陷入复杂性

发表于 更新于 分类于

这篇文章翻译自 Why Static Languages Suffer from Complexity，原文由 hirrolot 于 2022-01-19 发布在其个人博客。

image:https://hirrolot.github.io/media/content/why-static-languages-suffer-from-complexity/preview

编程语言设计社区的人们力图让语言更具“表达力”，尤其是通过强大的类型系统，以减少最终软件中的代码重复、提升易用性；然而，语言越是追求表达力，重复就越凶猛地渗入语言自身。

我称之为 静态-动态二象性（statics-dynamics biformity）：当你向语言引入一个新的语言学抽象时，它可能落在静态层、动态层，或者同时落在两者。前两种（只在某一层）会向语言引入 不一致性；后一种（两层各有一套）不可避免地引入 特性二象性。

在这里，静态层 是所有语言机制在编译期执行的地方；动态层 则是代码在运行期执行的地方。因此典型的控制流操作符（if/while/for/return）、数据结构与过程是动态的，而静态类型系统特性、语法宏是静态的。本质上，大多数静态语言抽象在动态空间都有对应物，反之亦然：

动态 (Dynamics) 静态 (Statics)

Array

Record type / Tuple / 异质列表 HList

Tree (数据结构)

Sum type / Coproduct

Value

泛型 / 关联类型 [1]

Loop / 递归

类型层归纳 (type-level induction)

If-then-else / 模式匹配

多个 trait 实现 (multiple trait impls)

函数签名

trait F<In…​> { type Out; }

函数实现

impl F<…​> for T { type Out = …​; }

函数调用

<T as F<…​>>::Out

接下来，在进一步阐述问题之前，让我展示如何用静态与动态两种方式实现逻辑等价的程序。大多数示例使用 Rust，但也适用于其它拥有足够表达力类型系统的通用语言；请记住，本文与具体实现无关，而 编程语言理论（PLT）相关。如果你很忙，可以直接跳到 主章节 看问题阐释。

记录类型 (Record type) — 数组 (Array)

来看日常的记录类型操作 (playground):

automobile-static.rs
struct Automobile {
    wheels: u8,
    seats: u8,
    manufacturer: String,
}

fn main() {
    let my_car = Automobile {
        wheels: 4,
        seats: 4,
        manufacturer: String::from("X"),
    };

    println!(
        "My car has {} wheels and {} seats, and it was made by {}.",
        my_car.wheels, my_car.seats, my_car.manufacturer
    );
}

同样的事可以用数组完成 (playground):

automobile-dynamic.rs
use std::any::Any;

#[repr(usize)]
enum MyCar {
    Wheels,
    Seats,
    Manufacturer,
}

fn main() {
    let my_car: [Box<dyn Any>; 3] = [Box::new(4), Box::new(4), Box::new("X")];

    println!(
        "My car has {} wheels and {} seats, and it was made by {}.",
        my_car[MyCar::Wheels as usize]
            .downcast_ref::<i32>()
            .unwrap(),
        my_car[MyCar::Seats as usize].downcast_ref::<i32>().unwrap(),
        my_car[MyCar::Manufacturer as usize]
            .downcast_ref::<&'static str>()
            .unwrap()
    );
}

是的，如果对 .downcast_ref 指定了错误类型，就会 panic。但程序的 逻辑 不变，只是把类型检查提升到了运行期。

更进一步，我们可以用异质列表 (heterogeneous list) 来编码静态的 Automobile：

automobile-hlist.rs
use frunk::{hlist, HList};

struct Wheels(u8);
struct Seats(u8);
struct Manufacturer(String);
type Automobile = HList![Wheels, Seats, Manufacturer];

fn main() {
    let my_car: Automobile = hlist![Wheels(4), Seats(4), Manufacturer(String::from("X"))];

    println!(
        "My car has {} wheels and {} seats, and it was made by {}.",
        my_car.get::<Wheels, _>().0,
        my_car.get::<Seats, _>().0,
        my_car.get::<Manufacturer, _>().0
    );
}

这一版本与 automobile-static.rs 执行了完全相同的类型检查，但还额外提供了将 type Automobile 当作普通集合来操作的 方法！例如，我们可以反转汽车字段 [2]：

assert_eq!(
    my_car.into_reverse(),
    hlist![Manufacturer(String::from("X")), Seats(4), Wheels(4)]
);

或者把我们的车与他们的车 zip：

let their_car = hlist![Wheels(6), Seats(4), Manufacturer(String::from("Y"))];

assert_eq!(
    my_car.zip(their_car),
    hlist![
        (Wheels(4), Wheels(6)),
        (Seats(4), Seats(4)),
        (Manufacturer(String::from("X")), Manufacturer(String::from("Y")))
    ]
);

……等等。

然而，有时我们希望把类型层计算应用到普通的 struct 与 enum 上，但做不到，因为我们无法仅根据类型名称提取其定义结构（字段及其类型 / 变体及其函数签名），特别是当该类型来自外部 crate 而无法加派生宏 [3]。为解决此问题，Frunk 开发者创建了一个过程宏，通过为类型实现 Generic trait 来检查其内部结构；它有一个关联类型 type Repr，实现后等价于某种可操作的异质列表。尽管如此，其它没有派生该宏的类型（尤其是透明的，如 DTO）仍然无法被检查，这归因于 Rust 上述的局限。

image:https://hirrolot.github.io/media/content/why-static-languages-suffer-from-complexity/rust-meme

和类型 (Sum type) — 树 (Tree)

有人会觉得用和类型表示 AST 节点很好 (playground):

ast-static.rs
use std::ops::Deref;

enum Expr {
    Const(i32),
    Add(Box<Expr>, Box<Expr>),
    Sub(Box<Expr>, Box<Expr>),
    Mul(Box<Expr>, Box<Expr>),
    Div(Box<Expr>, Box<Expr>),
}

use Expr::*;

fn eval(expr: &Box<Expr>) -> i32 {
    match expr.deref() {
        Const(x) => *x,
        Add(lhs, rhs) => eval(&lhs) + eval(&rhs),
        Sub(lhs, rhs) => eval(&lhs) - eval(&rhs),
        Mul(lhs, rhs) => eval(&lhs) * eval(&rhs),
        Div(lhs, rhs) => eval(&lhs) / eval(&rhs),
    }
}

fn main() {
    let expr: Expr = Add(
        Const(53).into(),
        Sub(
            Div(Const(155).into(), Const(5).into()).into(),
            Const(113).into(),
        )
        .into(),
    );

    println!("{}", eval(&expr.into()));
}

同样的事可以用带标签的树来做 (playground):

ast-dynamic.rs
use std::any::Any;

struct Tree {
    tag: i32,
    value: Box<dyn Any>,
    nodes: Vec<Box<Tree>>,
}

const AST_TAG_CONST: i32 = 0;
const AST_TAG_ADD: i32 = 1;
const AST_TAG_SUB: i32 = 2;
const AST_TAG_MUL: i32 = 3;
const AST_TAG_DIV: i32 = 4;

fn eval(expr: &Tree) -> i32 {
    let lhs = expr.nodes.get(0);
    let rhs = expr.nodes.get(1);

    match expr.tag {
        AST_TAG_CONST => *expr.value.downcast_ref::<i32>().unwrap(),
        AST_TAG_ADD => eval(&lhs.unwrap()) + eval(&rhs.unwrap()),
        AST_TAG_SUB => eval(&lhs.unwrap()) - eval(&rhs.unwrap()),
        AST_TAG_MUL => eval(&lhs.unwrap()) * eval(&rhs.unwrap()),
        AST_TAG_DIV => eval(&lhs.unwrap()) / eval(&rhs.unwrap()),
        _ => panic!("Out of range"),
    }
}

fn main() {
    let expr = /* Construction omitted... */;

    println!("{}", eval(&expr));
}

类似我们对 struct Automobile 所做的，我们也可以用 frunk::Coproduct 来表示 enum Expr。留作读者练习。

值 (Value) — 关联类型 (Associated type)

我们想用标准运算符 ! 取布尔值反 (playground):

negate-dynamic.rs
fn main() {
    assert_eq!(!true, false);
    assert_eq!(!false, true);
}

同样可以用关联类型来完成 [4] (playground):

negate-static.rs
use std::marker::PhantomData;

trait Bool {
    type Value;
}

struct True;
struct False;

impl Bool for True { type Value = True; }
impl Bool for False { type Value = False; }

struct Negate<Cond>(PhantomData<Cond>);

impl Bool for Negate<True> {
    type Value = False;
}

impl Bool for Negate<False> {
    type Value = True;
}

const ThisIsFalse: <Negate<True> as Bool>::Value = False;
const ThisIsTrue: <Negate<False> as Bool>::Value = True;

事实上，Rust 类型系统的图灵完备性 就建立在这个原则上，再配合类型归纳（稍后可见）。每当你看到一个普通值，要知道它在类型层都有形式对应物（在计算意义上）。每当你写一个算法，它都可以在类型层用概念等价的构造来“对应”！如果你想知道 如何做到，上面那篇文章给出了 数学证明：作者先用 动态层（和类型、模式匹配、递归）实现一个名为 Smallfuck 的东西，再用 静态层（trait 逻辑、关联类型等）实现。

递归 (Recursion) — 类型层归纳 (Type-level induction)

再看一个例子——但这次系好安全带 (playground)！

peano-dynamic.rs
use std::ops::Deref;

#[derive(Clone, Debug, PartialEq)]
enum Nat {
    Z,
    S(Box<Nat>),
}

fn add(lhs: &Box<Nat>, rhs: &Box<Nat>) -> Nat {
    match lhs.deref() {
        Nat::Z => rhs.deref().clone(), // I
        Nat::S(next) => Nat::S(Box::new(add(next, rhs))), // II
    }
}

fn main() {
    let one = Nat::S(Nat::Z.into());
    let two = Nat::S(one.clone().into());
    let three = Nat::S(two.clone().into());

    assert_eq!(add(&one.into(), &two.into()), three);
}

这是自然数的 Peano 编码。在 add 函数中，我们用递归计算和，用模式匹配决定何时停止。

由于递归对应类型归纳、模式匹配对应多个实现（impl），所以同样的事可以在编译期完成 (playground):

peano-static.rs
use std::marker::PhantomData;

struct Z;
struct S<Next>(PhantomData<Next>);

trait Add<Rhs> {
    type Result;
}

// I
impl<Rhs> Add<Rhs> for Z {
    type Result = Rhs;
}

// II
impl<Lhs: Add<Rhs>, Rhs> Add<Rhs> for S<Lhs> {
    type Result = S<<Lhs as Add<Rhs>>::Result>;
}

type One = S<Z>;
type Two = S<One>;
type Three = S<Two>;

const THREE: <One as Add<Two>>::Result = S(PhantomData);

这里，impl …​ for Z 是基例（终止条件），impl …​ for S< Lhs > 是归纳步（递归情况）——类似我们用 match 做的那样。归纳通过把第一个参数向 Z 归约来起作用：<Lhs as Add<Rhs>>::Result 就像 add(next, rhs)——再次触发“模式匹配”推进计算。注意这两个 trait 实现确实属于同一个逻辑函数；它们看似分离，是因为我们在类型层对数字 (Z 与 S<Next>) 做模式匹配。这与 Haskell 中的写法类似，每个模式匹配分支看上去像独立函数定义：

peano-static.hs
import Control.Exception

data Nat = Z | S Nat deriving Eq

add :: Nat -> Nat -> Nat
add Z rhs = rhs -- I
add (S next) rhs = S(add next rhs) -- II

one = S Z
two = S one
three = S two

main :: IO ()
main = assert ((add one two) == three) $ pure ()

类型层逻辑实体化 (Type-level logic reified)

image:https://hirrolot.github.io/media/content/why-static-languages-suffer-from-complexity/chad-meme

本文目的只是传达静态-动态二象性的直觉，而非提供形式化证明——后者请参考一个很棒的库 type-operators（同一个实现了 Smallfuck 在类型层运行的人）。本质上，它是一个算法宏 eDSL，归结为用 trait 做类型层操作：你可以定义代数数据类型并对其执行数据操作，和你在 Rust 中常规做法类似，但最终整个代码都驻留在类型层。更多细节见其 翻译规则 及作者写的 优秀指引。另一个值得一提的项目是 Fortraith，“一个在编译期把 Forth 编译为编译期 trait 表达式的‘编译期编译器’”：

forth!(
    : factorial (n -- n) 1 swap fact0 ;
    : fact0 (n n -- n) dup 1 = if drop else dup rot * swap pred fact0 then ;
    5 factorial .
);

上述代码把一个简单的阶乘实现翻译为基于 trait 与关联类型的计算。随后，你可以这样获得结果：

println!(
    "{}",
    <<<Empty as five>::Result as factorial>::Result as top>::Result::eval()
);

综上，无论你怎么称呼：静态还是动态，逻辑 部分保持不变。

静态所带来的不幸后果 (The unfortunate consequences of being static)

Are you quite sure that all those bells and whistles, all those wonderful facilities of your so called powerful programming languages, belong to the solution set rather than the problem set?

— Edsger Dijkstra (Edsger Dijkstra, n.d.)

当今编程语言关注的不是逻辑本身，而是逻辑之下的机制；它们认为布尔取反是最简单、必须从一开始就有的操作符，但 负 trait 约束（negative trait bounds） 却被视为“有很多问题”的可辩概念。大多数主流语言在标准库里支持树这种数据结构，但 sum type 却几十年未实现。我无法想象没有 if 的语言，但只有少数拥有完善的 trait 约束，更别提模式匹配了。这就是 不一致性 ——它迫使工程师设计低质量 API：要么走动态路线只暴露少量编译期检查，要么走静态路线试图规避宿主语言根本限制，使得使用愈发晦涩。把静态与动态组合到一个工作方案里也很复杂，因为你无法在静态上下文中调用动态。套用 函数颜色 的说法，动态是红色，静态是蓝色。

除了这种不一致，我们还有 特性二象性。在 C++、Haskell、Rust 等语言，这种二象性达到了最扭曲的程度；可以把任意所谓“有表达力”的语言视作两个或更多小语言拼接：C++ 语言本身与 C++ 模板/宏，Rust 语言与类型层 Rust + 声明式宏……在这种模式下，你每次在元层写点东西，都不能在宿主语言重用，反之亦然，违反 DRY 原则（稍后我们会看到）。此外，二象性增加学习曲线、阻碍语言演进，并最终走向特性膨胀——只有“入门教徒”才能看懂代码。看看任意 Haskell 生产代码，你会立刻看到一堆 GHC #LANGUAGE 子句，每一个都代表一个独立语言扩展：

feature-bloat.hs
{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE ViewPatterns               #-}

>> 改编自 haskell/haskell-language-server。

当宿主语言没有提供足够静态能力以便于开发时，一些程序员会更加疯狂地在其之上构建全新的编译期元语言和 eDSL。于是，不一致拥有转化为二象性的诡异属性：

  • [C++] 出现了复制 C++ 功能供元层使用的 模板元编程 库，如 Boost/Hana 与 Boost/MPL：

    take_while.cpp
    BOOST_HANA_CONSTANT_CHECK(
    hana::take_while(hana::tuple_c<int, 0, 1, 2, 3>, hana::less.than(2_c))
    ==
    hana::tuple_c<int, 0, 1>
);

    >> 改编自 hana/example/take_while.cpp。

    filter.cpp
    constexpr auto is_integral =
    hana::compose(hana::trait<std::is_integral>, hana::typeid_);

static_assert(
    hana::filter(hana::make_tuple(1, 2.0, 3, 4.0), is_integral)
    == hana::make_tuple(1, 3), "");
static_assert(
    hana::filter(hana::just(3), is_integral)
    == hana::just(3), "");
BOOST_HANA_CONSTANT_CHECK(
    hana::filter(hana::just(3.0), is_integral) == hana::nothing);

    >> 改编自 hana/example/filter.cpp。

    iter_fold.cpp
    typedef vector_c<int, 5, -1, 0, 7, 2, 0, -5, 4> numbers;
typedef iter_fold<
    numbers,
    begin<numbers>::type,
    if_<less<deref<_1>, deref<_2>>, _2, _1>
>::type max_element_iter;

BOOST_MPL_ASSERT_RELATION(
    deref<max_element_iter>::type::value, ==, 7);

    >> 改编自 MPL 文档。

  • [C] 我自己的编译期元编程框架 Metalang99 通过（滥）用 C 预处理器做类似事情。程度之深以至于我被迫字面意义地 重实现递归，利用类似 Lisp 的 trampoline 与 续延传递风格（CPS）技巧。最终我在标准库里有一大堆列表函数，如 ML99_listMap、ML99_listIntersperse、ML99_listFoldr，某种意义上使 Metalang99 作为纯数据转换语言比 C 本身更“有表达力” [5]

  • [Rust] 在第一个不一致性示例（Automobile）中，我们使用了 Frunk 库的异质列表。不难看出 Frunk 复制了 一些集合与迭代器功能，只是为了把它们提升到类型层。若能对异质列表应用 Iterator::map 或 Iterator::intersperse 会很酷，但做不到。更糟糕的是，如果我们仍想做声明式类型层数据转换，只能维护迭代器适配器与类型层对应物的 1:1 映射；每当迭代器新增一个工具，我们的 hlist 就少一个工具。

  • [Rust] Typenum 是另一个流行的类型层库：通过把整数编码成泛型 [6] 在编译期执行整型计算。这样，语言中负责整数的部分在静态层找到了副本，引入更多二象性 [7]。我们不能直接用 (2 + 2) * 5 给类型参数化，只能写成 <<P2 as Add<P2>>::Output as Mul<P5>>::Output！最好的办法就是写个宏替你干脏活，但那只是语法糖——你仍会面对上述 trait 带来的成堆编译错误。

image:https://hirrolot.github.io/media/content/why-static-languages-suffer-from-complexity/tmp-meme

有时，工程师觉得语言在动态代码里都太原始以致无法表达想法。但他们不放弃：

回想著名的 Greenspun 第十条，这种手工元语言通常“临时拼凑、非正式、漏洞百出且缓慢”，语义含糊、文档糟糕。元语言抽象 概念根本不起作用，尽管起初“用一个高度声明式的小领域专用语言表达问题域”的理由听上去很酷。当一个问题域（或某些中间机制）用宿主语言表达时，你只需理解如何串联函数调用来完成任务——这就是所谓 API；但当该 API 用另一种语言编写时，除了调用序列，还得理解那种语言的语法与语义，这在两方面都很不幸：加重心智负担、能维护此类元语言的开发者极少。以我的经验，手工元语言倾向于迅速失控并蔓延整个代码库，使得入门更难。不仅推理受损，编译器-开发者交互也受损：你是否尝试过使用复杂的类型或宏 API？如果是，你必然熟悉那种晦涩难懂的编译器诊断，可用下面的截图概括 [8]：

image:https://hirrolot.github.io/media/content/whats-the-point-of-the-c-preprocessor-actually/2

悲哀的是，如今“有表达力”的语言似乎意味着：“嗨，我把特性数量搞得一团糟，但没关系！”

最后，还得提一下在宿主语言里的元编程。借助 Template Haskell 与 Rust 过程宏 之类的模板系统，我们能用同样的语言操作宿主语言的 AST [9]，这对减少二象性是好事，却加剧一般语言不一致。宏不是函数：我们不能对宏做部分应用并得到一个部分应用的函数（或反之），因为它们就是不同概念——如果你要设计一个泛型、易用的库 API，这会很痛。就个人而言，我确实认为 Rust 的过程宏是一个 巨大的设计失误，与 C 里的 #define 宏相提并论：除了纯语法外，宏系统对被操纵的语言一无所知；你得到的不是一个优雅扩展语言的工具，而只是稍微增强的文本替换而已 [10]。例如，设想有一个枚举 Either，定义如下：

either.rs
pub enum Either<L, R> {
    Left(L),
    Right(R),
}

>> 改编自 either::Either。

现在设想有任意一个 trait Foo，我们想为 Either<L, R> 实现它，前提是 L 与 R 都实现了 Foo。事实是，我们不能仅凭名称给 Either 加一个为其实现此 trait 的派生宏，因为宏必须知道 Foo 的所有签名。更糟糕的是，Foo 可能定义在另一个库里，意味着我们无法在其定义上添加额外元信息以支持对 Either<L, R> 的派生。虽看似少见，其实并非如此；强烈建议看看 tokio-util 的 Either——它与上面枚举 完全相同，但实现了 Tokio 特定的 trait，如 AsyncRead、AsyncWrite、AsyncSeek 等 [11] 现在想象你的项目里来自不同库的五个不同 Either——那才是真正的集成噩梦！ [12] 虽然类型内省可能是折中方案，但它依旧会让语言比现在更复杂。

Idris：出路？ (Idris: The way out?)

One of the most fundamental features of Idris is that types and expressions are part of the same language — you use the same syntax for both.

— Edwin Brady, the author of Idris (Edwin Brady, n.d.)

让我们想一想怎样绕开问题。如果我们让语言彻底动态化，可以消灭二象性与不一致性 [13]，但会立即失去编译期验证的乐趣，最终在午夜调试程序。动态类型系统的悲惨众所周知。

唯一的途径是做一门语言，使其特性同时既是静态又是动态，而不要把同一个特性拆成两半。因此，理想的语言学抽象应当同时具备静态与动态；然而它仍是单一概念，而不是两个逻辑相似但接口不同的概念 [14]。一个完美例子是 CTFE，俗称 constexpr：同一份代码可以在静态上下文里于编译期执行，也可以在动态上下文里（例如从 stdin 请求用户输入时）运行；因此，我们不用为编译期（静态）与运行期（动态）各写一份代码，而是使用同一表示。

我见过的一个可能方案是依赖类型（dependent types）。借助依赖类型，我们可以令类型参数化不只是其它类型，还能是值。在一门依赖类型语言 Idris 中，有一个类型叫 Type——代表“所有类型的类型”，从而 弱化类型层与值层的二分。拥有如此强大的东西，我们可以表达 有类型的 抽象，它们通常要么内建在语言编译器/环境，要么通过宏实现。或许最常见、最具描述性的例子是一个类型安全的 printf，它可即席计算其参数类型，让我们在 Idris 中享受掌握它的乐趣 [15]！

首先，定义一个归纳数据类型 Fmt 及从格式字符串得到它的方法：

data Fmt = FArg Fmt | FChar Char Fmt | FEnd

toFmt : (fmt : List Char) -> Fmt
toFmt ('*' :: xs) = FArg (toFmt xs)
toFmt (  x :: xs) = FChar x (toFmt xs)
toFmt [] = FEnd

稍后我们会用它为 printf 生成类型。语法很像 Haskell，读者应易于理解。

现在最有趣的部分：

PrintfType : (fmt : Fmt) -> Type
PrintfType (FArg fmt) = ({ty : Type} -> Show ty => (obj : ty) -> PrintfType fmt)
PrintfType (FChar _ fmt) = PrintfType fmt
PrintfType FEnd = String

这个函数做什么？它 基于输入参数 fmt 计算一个类型。像往常一样，我们把 fmt 拆成三个情形分别处理：

  1. (FArg fmt)。由于 FArg 表示我们需要提供一个可打印实参，该分支生成一个额外参数的类型签名：

    1. {ty : Type} 表示 Idris 将自动推导该实参的类型 ty（隐式参数）。

    2. Show ty 是类型约束，声明 ty 必须实现 Show。

    3. (obj : ty) 是我们必须提供给 printf 的可打印实参。

    4. PrintfType fmt 是递归调用，处理剩余输入 fmt。在 Idris 中，归纳数据由归纳函数管理！

  2. (FChar _ fmt)。FChar 表示格式字符串中的普通字符，所以这里我们直接忽略它并继续 PrintfType fmt。

  3. FEnd。这是输入结束。我们希望 printf 产生 String，因此返回普通类型 String。

现在假设格式字符串为 "*x*"，即 FArg (FChar ('x' (FArg FEnd)))；PrintfType 会生成什么类型？简单：

  1. FArg：{ty : Type} -> Show ty => (obj : ty) -> PrintfType (FChar ('x' (FArg FEnd)))

  2. FChar：{ty : Type} -> Show ty => (obj : ty) -> PrintfType (FArg FEnd)

  3. FArg：{ty : Type} -> Show ty => (obj : ty) -> {ty : Type} -> Show ty => (obj : ty) -> PrintfType FEnd

  4. FEnd：{ty : Type} -> Show ty => (obj : ty) -> {ty : Type} -> Show ty => (obj : ty) -> String

很酷，现在到了编写梦寐以求 printf 的时候：

printf : (fmt : String) -> PrintfType (toFmt $ unpack fmt)
printf fmt = printfAux (toFmt $ unpack fmt) [] where
    printfAux : (fmt : Fmt) -> List Char -> PrintfType fmt
    printfAux (FArg fmt) acc = \obj => printfAux fmt (acc ++ unpack (show obj))
    printfAux (FChar c fmt) acc = printfAux fmt (acc ++ [c])
    printfAux FEnd acc = pack acc

可以看到，PrintfType (toFmt $ unpack fmt) 出现在类型签名中，意味着整个 printf 的类型 依赖于输入参数 fmt！但 unpack fmt 是什么？由于 printf 接受 fmt : String，我们应先把它转换为 List Char，因为在 toFmt 中我们要匹配该字符串；据我所知 Idris 不能用同样方式直接匹配普通 String。同理，在调用 printfAux 前也要 unpack fmt，因为它也以 List Char 作为结果累加器。

来查看 printfAux 的实现：

  1. (FArg fmt)。这里返回一个 lambda，接收 obj 并对其调用 show，然后用 ++ 运算符追加到 acc。

  2. (FChar c fmt)。只需把 c 追加到 acc 并再次对 fmt 调用 printfAux。

  3. FEnd。由于 acc 类型是 List Char 而我们必须返回 String（根据 PrintfType 的最后一个分支），所以对它调用 pack。

最后，测试 printf：

printf.idr
main : IO ()
main = putStrLn $ printf "Mr. John has * contacts in *." 42 "New York"

它输出 Mr. John has 42 contacts in "New York".。但如果我们不提供 42 呢？

Error: While processing right hand side of main. When unifying:
    ?ty -> PrintfType (toFmt [assert_total (prim__strIndex "Mr. John has * contacts in *." (prim__cast_IntegerInt (natToInteger (length "Mr. John has * contacts in *.")) - 1))])
and:
    String
Mismatch
between: ?ty -> PrintfType (toFmt [assert_total (prim__strIndex "Mr. John has * contacts in *." (prim__cast_IntegerInt (natToInteger (length "Mr. John has * contacts in *.")) - 1))]) and String.

test:21:19--21:68
 17 |     printfAux (FChar c fmt) acc = printfAux fmt (acc ++ [c])
 18 |     printfAux FEnd acc = pack acc
 19 |
 20 | main : IO ()
 21 | main = putStrLn $ printf "Mr. John has * contacts in *." "New York"
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: compiling hole Main.main

是的，Idris 发现错误并产生类型不匹配！这基本上就是你用一等类型实现类型安全 printf 的方式。如果你好奇 Rust 中的同样东西，请看看 Will Crichton 的尝试，它严重依赖我们上文看到的异质列表。这种做法的缺点现在应该非常清楚：在 Rust 中，类型系统的语言与主语言不同；而在 Idris 中，它确实是同一套——这就是为什么我们可以自由地把类型层函数定义为返回 Type 的常规函数，并在类型签名中调用它们。此外，因为 Idris 是依赖类型的，甚至可以基于某个运行期参数计算一个类型，这在 Zig 之类的语言中是不可能的。

image:https://hirrolot.github.io/media/content/why-static-languages-suffer-from-complexity/printf-meme

我已经预见了问题：用宏实现 printf 有什么问题？毕竟 println! 在 Rust 里运行得很好。问题在于宏。想想：为何一门编程语言需要重量级宏？因为我们可能想扩展它。我们为何想扩展它？因为语言无法满足需求：我们无法用常规语言学抽象表达某些东西，所以决定用特设元抽象扩展语言。在主体部分，我已经论述了这种方式为何糟糕——因为宏系统对被操作语言一无所知；事实上，Rust 的过程宏只是 M4 预处理器 的花哨名字。你们把 M4 集成进语言。当然，这 比外部 M4 好，但仍是 20 世纪的方法；过程宏甚至不能操作一个 抽象语法树，因为 syn::Item——写过程宏常用结构——确切说是一个 具体语法树，或“解析树”。另一方面，类型是宿主语言的自然组成部分，这就是为什么如果我们能用类型表达一个程序抽象，我们就在 重用 语言学抽象，而非求助特设机械。理想情况下，语言应该没有宏，或只有轻量语法改写规则（比如 Scheme 的 extend-syntax 或 Idris 的 语法扩展），以保持一致性并适合解决预期任务。

这么说来，Idris 通过引入 “所有类型的类型” Type，抹去了第一层“值-泛型”的二象性。这样也解决了许多其它对应，如递归 vs. 类型层归纳、函数 vs. trait 机制，等等；这反过来让我们即便在高度泛型代码中，也尽可能用同一门语言编程。比如，你甚至可以把类型列表表示为 List Type，就像 List Nat 或 List String，并照常处理！这是由于一个 累积宇宙层级：简单说，Type 的类型是 Type 1，Type 1 的类型是 Type 2，以此类推。由于 Data.List 的泛型参数 a “隐式” 类型为 Type，它既可以是 Nat、String 也可以是 Type；在后者情况下，a 会被推导为 Type 1。这种无限类型序列是为了避免 罗素悖论 的变体，使得一个值在结构上“比它的类型更小”。

然而，Idris 并不简单。我们那二十行的 printf 示例已经用到“一整套特性”，诸如归纳数据类型、依赖模式匹配、隐式参数、类型约束等。此外 Idris 还具备 计算效应、elaborator 反射、余归纳（coinductive）数据类型以及用于定理证明的大量工具。面对如此繁多的类型设施，你往往在摆弄语言机器，而不是做有意义的工作。我几乎不相信以当前状态，依赖类型会在生产中大规模使用；目前在编程世界里，它们还不过是 PL 研究者与随机爱好者的玩具。仅有依赖类型实在太底层了。

Zig：更简单，但过于“系统级” (Zig: Simpler, but too systems)

In Zig, types are first-class citizens. They can be assigned to variables, passed as parameters to functions, and returned from functions.

— The Zig manual (Zig developers, n.d.)

最后一位“病人”是 Zig 编程语言。下面是一个 Zig 的编译期 printf 实现（抱歉暂时没有高亮）：

printf.zig
const std = @import("std");

fn printf(comptime fmt: []const u8, args: anytype) anyerror!void {
    const stdout = std.io.getStdOut().writer();

    comptime var arg_idx: usize = 0;

    inline for (fmt) |c| {
        if (c == '*') {
            try printArg(stdout, args[arg_idx]);
            arg_idx += 1;
        } else {
            try stdout.print("{c}", .{c});
        }
    }

    comptime {
        if (args.len != arg_idx) {
            @compileError("Unused arguments");
        }
    }
}

fn printArg(stdout: std.fs.File.Writer, arg: anytype) anyerror!void {
    if (@typeInfo(@TypeOf(arg)) == .Pointer) {
        try stdout.writeAll(arg);
    } else {
        try stdout.print("{any}", .{arg});
    }
}

pub fn main() !void {
    try printf("Mr. John has * contacts in *.\n", .{ 42, "New York" });
}

这里，我们使用了一个特性 comptime：一个标记为 comptime 的函数参数 必须 在编译时已知。它不仅允许激进的优化，还打开了一座“元编程”英灵殿（Valhalla），尤其是不需要独立的宏层或类型层子语言。以上代码无需更多解释——平凡直接的逻辑对每个程序员都很清晰，不像看起来像“疯癫天才幻想产物”的 printf.idr。

如果我们省略 42，Zig 会报编译错误：

An error occurred:
/tmp/playground2454631537/play.zig:10:38: error: field index 1 outside tuple 'struct:33:52' which has 1 fields
            try printArg(stdout, args[arg_idx]);
                                     ^
/tmp/playground2454631537/play.zig:33:15: note: called from here
    try printf("Mr. John has * contacts in *.\n", .{ "New York" });
              ^
/tmp/playground2454631537/play.zig:32:21: note: called from here
pub fn main() !void {
                    ^

我在编写 printf 时唯一的不便是那些 巨量错误…… 很像 C++ 模板。不过我承认这可以通过更显式的类型约束来解决（或至少规避）。总体上，Zig 的类型系统设计是合理的：有一个称为 type 的“所有类型的类型”，并且借助 comptime，我们可以在编译期通过普通变量、循环、过程等 计算类型。我们甚至可以通过内建的 @typeInfo、@typeName 与 @TypeOf 做类型反射！是的，我们不再能依赖运行期值，但如果你不需要一个定理证明器，完整的依赖类型可能就是杀鸡用牛刀。

image:https://hirrolot.github.io/media/content/why-static-languages-suffer-from-complexity/types-meme

一切都很好，除了 Zig 是一门系统语言。在 官网 上，Zig 被描述为“一门通用编程语言”，但我很难同意。是的，你几乎可以用 Zig 写任何软件，但 该不该？我在 Rust 与 C99 中维护高层代码的经验告诉我：不该。第一，安全性：如果你把一门系统语言做“安全”，你会让程序员与借用检查器（borrow checker）和所有权（或等价机制）周旋——这与业务逻辑毫无关系（相信我，我懂那种痛）；否则，若你选择 C 式手工内存管理，你会让程序员花长时间调试，只希望 -fsanitize=address 能给点有用信息。此外，如果你想在指针之上构建新抽象，最后会得到 &str、AsRef<str>、Borrow<str>、Box<str> 等等。拜托，我只想要一个 UTF-8 字符串；大多数时候并不关心是哪种变体。

第二个理由涉及语言运行时 [16]：为了使语言是“系统级”的，并避免隐藏的性能惩罚，它应当有最小化的 runtime——没有默认 GC、没有默认事件循环等，但对于特定应用（比如异步）却可能需要 runtime——因此你实际上 必须 以某种方式处理自定义 runtime 代码。这里我们会遇到一整套关于 函数颜色 的问题 [17]：例如，语言里有了 async 却没有工具去 抽象覆盖 同步与异步函数，这意味着你把语言分裂成两个部分：同步与异步；于是如果你有一个泛型高阶库，它将不可避免被标记为 async 以接受各种用户回调。要解决这个问题，你需要实现某种 效应多态（例如 monad 或代数效应），而这仍是研究课题。高级语言天生要处理的问题更少，这就是为什么大多数软件写在 Java、C#、Python、JavaScript；在 Golang 中，概念上每个函数都是 async，从而 默认 促进一致性，而无需诉诸复杂类型特性。相反，Rust 已经被视为复杂语言，却仍没有标准方式编写真正泛型的异步代码。

Zig 仍可用于大型系统项目，比如浏览器、解释器与操作系统内核——没人希望这些东西意外挂起。Zig 的低层编程特性能方便地操作内存与硬件设备，而其理性的元编程方式（用得好）会孕育结构清晰的代码。把它带到高层代码只会增加心智负担而没有显著收益。

Progress is possible only if we train ourselves to think about programs without thinking of them as pieces of executable code.

— Edsger Dijkstra

最终感言 (Final words)

静态语言强制编译期检查；这很好。但它们饱受特性二象性与不一致性之苦——这很糟。动态语言在这方面的痛苦较轻，但缺乏编译期检查。一个假设的解决方案应当兼取两者之长。

编程语言理应被重新思考。

参考文献 (References)

Edsger Dijkstra. n.d. “On the Teaching of Programming, i.e. On the Teaching of Thinking.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD473.html.

Edwin Brady. n.d. “Type-Driven Development with Idris.” Manning Publications Co. https://www.manning.com/books/type-driven-development-with-idris.

Zig developers. n.d. “Introducing the Compile-Time Concept.” https://ziglang.org/documentation/0.9.0/#Introducing-the-Compile-Time-Concept.

1. 在诸如 构造演算 这样的系统中，多态函数把泛型当作 kind 为 *（“所有类型的 kind”）的普通函数参数来接受。
2. 需要给字段类型加上 #[derive(Debug, PartialEq)]
3. 除了不可扩展性之外，派生宏还带来 紧耦合：如果 DeriveX 放在 Foo 上，那么 foo.rs 不可避免地依赖 DeriveX。这会使组件迁移复杂化、拖慢编译时间并导致合并冲突。
4. 我们甚至可以在 Cond 上把这两个 Negate 实现泛化，但由于 Rust 类型系统的一个 已知 bug 目前做不到。
5. 在 C++ 社区有类似库 Boost/Preprocessor。
6. 还记得“变量-泛型”对应吗？
7. 不久前，最小可用的 const generics 已稳定。理论上可用相同整数表示替换 Typenum。
8. 写 teloxide 时遇到的，记不清了。
9. 严格来说，Rust 不能操作其真实 AST，但稍后再说。
10. 更新：我的意思是你可以操纵语法，但对语义一无所知。当然，Rust 宏比 C 宏方便得多，但在概念上两者几乎一样。
11. 更好笑的是，最初我写了一个三方 crate tokio-either，只包含那个 Either + 若干 trait 实现。后来 Tokio 维护者 决定 把它移到 tokio-util。
12. 更新：我不知道 Tokio 为什么不直接为 either::Either 实现其 trait，就像对 tokio-either 那样。不管怎样，这都不能消除必须手工“派生”的混乱。
13. Terra 是一个很好的简单动态语言例子。在 “Simplicity” 小节，他们展示了静态语言特性如何以库形式在动态语言中实现。
14. 多重人格障碍？🤨
15. 完整代码见 我的 gist。我用的是 Idris2，可在 这里 下载。
16. 在此语境下，语言运行时是把语言语义（即其抽象机）映射到真实执行器语义的隐藏机制。
17. 更新：有人讨论 Zig 是否 无颜色 或 有颜色。然而，即便 Zig 解决了函数着色问题，这也不改变我最初所说：在设计或编写系统语言时，你仍需处理在高级语言中微不足道的问题。