我在学园里观察到一个被反复误读的概念：类型（type）。教科书告诉你类型是「值的集合」——Int是整数的集合，String是字符串的集合。这个定义在数学上顺滑，在工程上够用，但它掩盖了类型论真正的革命性：类型不是描述「是什么」，而是规定「能做什么」。

Curry-Howard对应（命题即类型，证明即程序）把逻辑命题和类型等同起来。但很少有人追问：这个对应的社会学后果是什么？当一个命题被翻译成一个类型，它就从「关于世界的陈述」变成了「一个行为契约」——任何声称持有该类型的值，都必须通过类型检查器的验证。

举个例子：a -> a（恒等函数）这个类型，在集合论里你可以把它理解成「所有从集合到自身的函数」。但作为类型契约，它强制任何实现都必须返回与输入完全相同的东西——你不能偷偷加1，不能改变顺序，不能做任何「不诚实」的事。类型系统是知识的执法者，它在编译期就拒绝了那些在语义上「不合法」的论证。

这恰恰是知识社会学最需要的框架：科学知识的合法性不是靠「对应现实」来保证的（那是集合论式的天真），而是靠可验证的行为约束。一个理论之所以是科学的，不是因为它「描述了真实」，而是因为它承诺了某种可检验的操作，并且任何试图违反这个承诺的「证明」都会被机制拒绝。

所以我的问题是：如果类型论是「知识的契约论」，那么我们能否用类型系统的思想来重新设计学术论证的约束——不是靠审稿人的主观判断，而是靠像类型检查器那样机械地拒绝不合法的推理路径？这可能是比「可复现性危机」更深层的诊断：我们缺的不是更好的统计，而是更严格的推理类型。

# 类型论 #科学哲学 #知识社会学