Skip to content

programming-as-algebra.md

Latest commit

 

History

History
170 lines (119 loc) · 9.89 KB

programming-as-algebra.md

File metadata and controls

170 lines (119 loc) · 9.89 KB
Raw

编程的尽头是代数

Programming Converges to Algebra

程序建模不是在搭脚手架——是在发现领域中已经存在的数学结构。

§0 一个观察

大学软件工程教育教的是写法（syntax, patterns, frameworks），不教建模（algebra, types, categories）。但当你穿透所有技术表层，编程的尽头不是更好的设计模式、更新的框架——是数学。

$$\text{Good Program} \cong \text{Algebraic Structure of Domain}$$

好的程序与其领域的代数结构同构。这不是比喻。类型是集合，函数是态射，接口是全称量化，泛型是参数多态，枚举是余积。你每天在用的编程概念，本来就是数学概念的工业化包装。

§1 两条路径

§1.1 工业路径（自底向上）

大多数程序员的成长路径是自底向上的：

语法 → 设计模式 → 架构风格 → SOLID 原则 → ……然后撞墙

撞墙意味着：你感觉代码"不对"但说不清哪里不对，你感觉某个抽象"太粗"但找不到精确的判据，你感觉理想的设计"应该存在"但无法从现有工具中推导出来。

这些墙壁的共同根源是：缺少对领域的数学建模。设计模式是前人经验的归纳总结，但归纳永远不可能穷尽——当你的领域没有对应的模式时，归纳失效。

§1.2 数学路径（自顶向下）

另一条路径是自顶向下的：

领域的数学结构 → 类型代数编码 → 编译器验证 → 实现细节

先理解领域中存在哪些实体、它们之间的关系是什么、哪些组合合法哪些不合法——用集合、函数、代数恒等式精确描述。然后用类型系统将这个数学模型字面翻译为代码。

这条路径的关键洞见是：你不是在"设计"代码结构——你是在"发现"领域中本来就存在的数学结构，然后如实表达。 好的代码结构不是发明出来的，是从领域的数学中提取出来的。

§2 知识地图

§2.1 整体结构

以下知识构成一张连贯的图，而非孤立的碎片：

                    ┌─────────────────────────┐
                    │ 范畴论 (Category Theory) │
                    │ "最优抽象"的判定标准     │
                    └────────────┬────────────┘
                                 │
              ┌──────────────────┼──────────────────┐
              │                  │                  │
    ┌─────────▼──────┐  ┌───────▼────────┐  ┌──────▼───────────┐
    │ 类型论          │  │ 代数学          │  │ 逻辑学            │
    │ (Type Theory)  │  │ (Algebra)      │  │ (Logic)          │
    │ 类型即命题      │  │ 结构的组合学    │  │ 命题即类型        │
    └───────┬────────┘  └───────┬────────┘  └──────┬───────────┘
            │                   │                  │
            └─────────┬─────────┘      ┌───────────┘
                      │                │
            ┌─────────▼────────────────▼───┐
            │ Curry-Howard-Lambek 对应      │
            │ 逻辑 ≅ 类型 ≅ 范畴            │
            └─────────────┬────────────────┘
                          │
          ┌───────────────┼───────────────────────┐
          │               │                       │
  ┌───────▼──────┐ ┌──────▼───────┐ ┌────────────▼───────────┐
  │ ADT          │ │ 参数多态     │ │ 效果系统 / Session Types│
  │ 积+和=建模   │ │ 泛型=抽象    │ │ 能力=可组合的约束       │
  └───────┬──────┘ └──────┬───────┘ └────────────┬───────────┘
          │               │                      │
          └───────────────┼──────────────────────┘
                          │
              ┌───────────▼──────────────┐
              │ 基于能力的编程            │
              │ 能力的组合决定身份        │
              │ 编译器验证能力的可交互性  │
              └──────────────────────────┘

§2.2 各节点说明

节点 核心洞见 为什么重要
类型论 类型是命题，程序是证明。$f: A \to B$ 是"给定 $A$ 的证据可构造 $B$ 的证据" 编译器帮你证定理——你只需把定理写成类型签名
代数数据类型 (ADT) $A + B$（择一）和 $A \times B$（并列）是完备的建模原语 任何领域实体都可用积+和精确编码，无需 Option 地狱
参数多态 $\forall T.\ f(T)$ — 对所有类型成立的操作 消除复制粘贴，代码中的"定理"自然是泛型的
Curry-Howard 逻辑证明与类型化程序之间存在同构 编程不是"手艺"，是逻辑的可执行形式
范畴论 对象由其态射唯一确定（Yoneda 引理） 提供"抽象是否最优"的精确判据
效果系统 函数的副作用编码在类型中 纯函数与副作用函数不再靠文档区分——类型强制
Session Types 通信协议编码在类型中 协议违规在编译期被捕获
基于能力的编程 能力的组合决定身份——名字只是简称 ISP 不是设计规则而是数学推论，Option 地狱被彻底消灭

§3 为什么大学不教这些

计算机科学诞生时就分裂为数学路径（Church, Curry, Howard, Martin-Löf → λ演算, 类型论, ML/Haskell）和工程路径（GoF, Agile, OOP）。大学教的主要是工程路径的工业化产物。

ADT（1970s）、Curry-Howard（1958）、Yoneda（1954）不是前沿——是工业语言终于追上了数学。

这些知识难入教材还因为它们构成整体——不理解 ADT 就不知道 Option 地狱为何是错的，不理解 Yoneda 就不知道为何“能力即身份”。单独每片看起来像“过度抽象”，拼在一起才构成比设计模式更强大也更简单的编程范式。

§4 搜索关键词与推荐路径

入门层：algebraic data types, making illegal states unrepresentable (Yaron Minsky), parse don't validate (Alexis King), type-driven development (Edwin Brady), domain modeling made functional (Scott Wlaschin), capability-based security

中间层：Curry-Howard correspondence / propositions as types (Philip Wadler), theorems for free (Wadler), algebraic effects, session types, typeclass / trait coherence, phantom types

深层：Martin-Löf type theory, Yoneda lemma, initial algebra / F-algebra, free monad, category theory for programmers (Bartosz Milewski), HoTT

推荐路径 A（工程切入）：Domain Modeling Made Functional → Parse Don't Validate → Making Illegal States Unrepresentable → Propositions as Types (Wadler Strange Loop 2015) → Category Theory for Programmers

推荐路径 B（数学切入）：Haskell (typeclass + ADT) → TAPL (Pierce) → Category Theory for Programmers → Rust trait+enum 实践

§6 汇聚点

所有路径最终汇聚到同一个洞见：

$$\text{编程} = \text{发现领域的代数结构} + \text{用类型系统如实表达} + \text{让编译器验证正确性}$$

具体而言：

  1. 实体建模：领域中有什么东西？→ 类型
  2. 关系建模：它们之间什么关系？→ 函数、态射
  3. 约束建模：哪些组合合法哪些不合法？→ 类型约束、trait bound
  4. 操作建模：可以对它们做什么？→ 函数签名（类型是签名的一部分）
  5. 验证：编译器能检查多少？→ 越多越好

当这些步骤被严格执行时，你的代码就是领域数学的可执行实现。设计模式变得不需要——因为数学结构本身就是"模式"。重构变得机械——因为代数恒等式告诉你什么和什么同构。Bug 变得稀少——因为编译器在类型层面验证了大部分不变量。

编程的尽头不是更好的工具，是更清晰的数学。

§7 一个类比

结构力学告诉你梁能承受多少载荷——是数学计算，不是经验法则。 类型论告诉你代码能处理多少状态——是代数证明，不是设计模式。 SOLID 原则的每一条都可从类型论和范畴论中推导出来——反过来不行。

参考来源

类型 标题 作者
书 Types and Programming Languages Benjamin Pierce
书 Category Theory for Programmers Bartosz Milewski (免费在线)
书 Domain Modeling Made Functional Scott Wlaschin
书 Type-Driven Development with Idris Edwin Brady
书 Algebra of Programming Bird & de Moor
书 Software Abstractions Daniel Jackson
演讲 Propositions as Types Philip Wadler
论文 Theorems for Free Philip Wadler
文章 Parse, Don't Validate Alexis King
文章 Making Illegal States Unrepresentable Yaron Minsky