知识社会学里有个经典困境：我们以为分类系统是描述性的——先有世界，再有标签。但类型论者会告诉你，分类只是个幻觉，真正起作用的是「类型」作为约束条件。

举一个语言学里最著名的例子：命题「鸟会飞」。在亚里士多德逻辑里，这是一个全称命题：∀x(Bird(x) → Fly(x))。但只要你见过一只企鹅，这个命题就死了。于是你开始修补：「鸟会飞，除了企鹅、鸵鸟、几维鸟……」——修补到最后，你得到的不是一个分类，而是一张豁免清单。

类型论给出了完全不同的读法：Bird 不是一堆个体的集合，而是一个「类型」。类型不是描述「是什么」，而是规定「能做什么」。在 Martin-Löf 类型论里，Bird 类型携带一个结构：它包含一个字段叫 locomotion，而这个字段的类型是 Flight | Flightless。于是「鸟会飞」不是一个可以被证伪的命题，而是一个「类型错误」（type error）——就像把字符串当整数相加。

这个转换的深刻之处在于：它把「世界是什么样的」这个本体论问题，转换成了「我们的语言允许我们怎么谈论世界」这个语言学问题。类型不是对自然的镜像，而是对言说的约束。

这让我想到科学哲学里 Kuhn 的「不可通约性」（incommensurability）：两个范式之间的分歧，往往不是关于事实的分歧，而是关于「什么算作合法陈述」的分歧。类型论给这个老问题提供了一个精确的模型：范式不是不同的信念集合，而是不同的类型系统——同一个词（「质量」「基因」「物种」）在两个系统里有着不同的类型签名。

所以我的问题是：如果「不可通约性」本质上是类型不匹配，那么跨范式的交流是否可能？还是说，我们只能在类型系统之间做「翻译」——而翻译的极限，正是类型论里那个著名的定理：不存在一个算法能判定任意两个类型是否相等？

# 语言类型学 #科学哲学 #知识社会学