当前位置：首页 > web >正文

CppCon 2014 学习:CONVERGENT EVOLUTION

web 2025/7/6 21:24:36

“这里没有什么重大发现

我要讲的内容其实都是大家比较熟悉的知识……
如果你读过不少相关论文，应该都知道这些东西。
如果你没看过相关论文，可能会觉得 concepts 只是为了简化模板错误信息而设计的。
但这些理念其实很酷！
我想把它们传播给大家，展示它们的酷炫之处。
也许能帮助你用一种新的角度去理解和推理你的程序。
这也说明，有时候设计中确实只有一个“正确”的方案。”
简单说就是，演讲者觉得这部分内容对内行来说是基础或常识，但对没深入了解的人来说可能会很新鲜。他想强调 concepts（C++中的概念）不仅仅是为了简化错误，而是有很强的思想和美感，值得大家了解和思考。同时，也传达了设计中“最佳方案”的理念。

*“程序就是证明”**

这被称为“柯里-霍华德对应”（Curry-Howard correspondence）。
类型（types）就是命题（propositions）。
某个类型的对象就是对该命题的一个证明。
这个理论在现实的编程语言中并不完全成立，尤其是C++。
因为有计算方式（evaluation scheme）、副作用（side effects）、甚至宇宙射线等不可控因素。
但偶尔用这种方式思考程序设计是很有趣的。
这种观点是否“有用”还不好说。
不过，这个理念确实把所有编程语言都联系起来了。
简单说，就是说“写程序和数学证明是相似的”，类型系统就像数学命题，写出符合某个类型的程序，就好像完成了对那个命题的证明。这是理论上的一种很优雅的观点，虽然现实里会有很多复杂因素影响，但它帮助我们理解编程语言的本质。

解释程序中的类型和语言结构，如何对应逻辑中的各种命题和逻辑连接词，这是“程序=证明”（柯里-霍华德对应）的一部分具体表现。详细理解如下：

1. 函数对应蕴含（Implications，IF）

逻辑中“如果A，则B”用 $\to B$ 表示。
在编程语言中，函数类型 $\to B$ 表示“从类型A到类型B的函数”。
例如：
- Haskell的函数类型写作 A -> B
- C语言中类似函数指针写作 B (*)(A)
- C++中的 std::function<B(A)> 可以看成这个意思

2. 聚合类型对应合取（Conjunction，AND）

逻辑中“且”，表示两个命题都成立。
在程序中，聚合类型（比如struct、tuple）包含了多个字段，必须同时满足所有字段类型。
例如：
- C++ struct { A a; B b; }
- Haskell或C++的元组 std::tuple<A, B>

3. 和类型对应析取（Disjunction，OR）

逻辑中的“或”，表示至少满足一个命题。
程序中的和类型（sum types）是联合类型，表示值可能是几种不同类型中的一种。
例如：
- C语言的联合体 union { A a; B b; }
- Haskell中的代数数据类型（ADT） data Foo = FooA A | FooB B

4. 参数多态对应“∀”（全称量词，For all）

逻辑中“对于所有…都成立”，
程序中的参数多态表示函数或类型适用于所有类型参数。
例如：
- Haskell: id :: forall a. a -> a，表示“对于所有类型a，id都是a到a的函数”
- C++模板：template<typename A> A id(A); 同样表示对任意类型A都成立

5. 存在类型对应“∃”（存在量词，Exists）

逻辑中表示“存在某个…使得…”
程序中的存在类型更复杂，一般表示值和类型的配对，隐藏具体类型细节。
例如：
- 书《Types and Programming Languages》(TaPL) 里说它们是值和类型的成对出现
- ML模块系统是存在类型的一个例子
- 存在类型可以用全称量词编码（用universals表达）

总结

程序类型和逻辑命题一一对应：
- 函数类型 = 蕴含 (if-then)
- 结构体/元组 = 合取 (and)
- 联合体/代数数据类型 = 析取 (or)
- 模板/泛型 = 全称量词 (forall)
- 存在类型 = 存在量词 (exists)

解释约束（Constraint）在程序设计，尤其是模板和泛型编程中的含义，结合逻辑证明的角度来理解。

什么是约束（Constraint）？

约束，简单说，就是你必须满足的附加条件，才能使用某个功能或模板。

举例说明：排序函数需要的约束

假设你要对一个集合排序，你必须证明这个集合的元素是“全序的”（total order），也就是说元素之间能比较大小，并且比较满足全序性质（比如反自反、传递性、全比较性等）。
C语言中的qsort函数：
```
void qsort(void *base, size_t num, size_t size, int (*compar)(const void *, const void *))
```
其中，compar函数指针负责两个元素的比较，告诉排序算法如何比较元素大小。
compar本质上是“证明”这个集合的元素满足全序的“证据”或“约束”。
你传给qsort的比较函数相当于告诉它：“这里有一个比较方法，可以确定元素的顺序。”

约束本质上是什么？

约束就是程序中额外的参数，用于表达对类型的附加要求。
在更高级的语言特性里，比如C++ Concepts，这些约束会用类型系统表达出来，确保只有满足条件的类型才能被模板实例化。

约束在逻辑上的对应

约束就是你在证明某个命题（程序正确性、函数适用性）时，用到的辅助引理（lemma）。
换句话说，它们是证明你程序正确或可用的“前提”或“条件”。

总结

约束 = 限制/条件 = 证明你能做某事的证据
在排序例子中，比较函数就是约束，证明元素可以比较，才能排序成功
约束让程序更安全，也能让编译器在编译期检查是否满足要求

为什么需要 Concepts（概念）或 Type Classes（类型类），核心原因是便利性和代码简洁。

为什么需要 Concepts / Type Classes？

方便（Convenience）
比如：
如果已经确定类型 T 的对象具备“全序关系”（total order）这个事实，那么排序函数就不应该每次调用时，都让你手动传入比较函数来“证明”这个事实。
减少重复劳动
你不应该每次用排序函数都要写那个比较器或证明，你只要声明这个类型本身已经具备这个性质，函数自动“知道”即可。
“从环境中获取”
就像开玩笑说的：“你叫函数‘Just F***ing Get It（JFGI）’”，意思是：函数应该自动从类型系统或上下文中获得这个证明，不需要人工额外提供。
类型类其实就是隐式参数
- 在Haskell和Scala中，类型类实际上是“按类型索引的隐式参数”。
- 也就是说，类型类是类型本身，也是一种“隐式传递的参数”，编译器自动查找符合约束的实例。
集中声明，广泛适用
Concepts 或 Type Classes 允许你把类型的“事实”（比如“类型T支持比较”）集中声明在一个地方，程序其他地方只要写出这个约束，编译器自动知道这个类型满足条件，无需每处重复声明。

总结

概念和类型类是为了让代码更简洁、易用，减少样板代码（boilerplate）
它们是类型系统中的“全局约束”，你声明一次，所有地方都自动生效
让泛型编程更自然，更安全，错误更早发现

通过 Haskell 和 C++ 两种语言对比，进一步说明了概念（Concepts）/类型类（Type Classes）的实际用法，体现了它们如何表达类型的约束。

Haskell 例子解析：

-- 排序函数声明，要求类型 a 必须实现 Ord 类型类（有序）
sort :: Ord a => [a] -> [a]
-- Ord 类型类继承 Eq 类型类，定义了 <= 操作符
class Eq a => Ord a where(<=) :: a -> a -> Bool
-- Eq 类型类定义了 == 操作符
class Eq a where(==) :: a -> a -> Bool

Ord a => 是约束，表示排序函数只能用在实现了 Ord 的类型 a 上。
Ord 继承自 Eq，确保比较大小之前能比较相等。
这样写的好处是，只要类型实现了这些接口，函数就能使用，无需每次都传入比较函数。

C++ 例子解析：

template<typename T> requires Ord<T>
list<T> sort(list<T>);
template<typename T>
concept boolOrd = requires (T a, T b) {{ a <= b } -> bool;  // T类型必须支持 <= 并返回 bool// 这里可以添加更多约束
};
template<typename T>
concept boolEq = requires (T a, T b) {{ a == b } -> bool;  // T类型必须支持 == 并返回 bool
};