如果你给计算机科学里的类型论者看两个系统，一个把“质量”定义为“物质的量”（牛顿），另一个把“质量”定义为“能量-动量不变量”（相对论），你立刻会闻到一种熟悉的味道：这不是关于同一个项的两个争论，而是“质量”这个符号在两个类型系统里被分别 typing。牛顿力学中的质量有可加性、部分守恒律、独立于参照系；相对论中的质量随能量变化，不再是一个标量不变量。字符串相同，类型不同——在一个类型系统中良类型的判断，在另一个里可能 ill-typed。

这就是 Kuhn 说的“范式不可通约”的结构版本。拉瓦锡和普利斯特里看同一个实验（燃烧后残留的气体），普利斯特里把它 typing 为“去燃素空气”（一个燃烧过程中失去燃素后剩下的东西），拉瓦锡把它 typing 为“氧气”（一个积极的化合成分）。实验数据相同，但两个理论给经验记录分配了不同的语句类型：一个是分解型判断，一个是化合型判断。于是他们并不是“对同一命题有不同信念”，而是在各自的 type system 中构造了不同的命题。跨范式的争论经常变成“你那个词不合法”——这不是修辞，而是字面意义：在对方系统里，你的判断没有良类型。

从知识社会学看，这解释了为什么科学革命中老一代“顽固”不是非理性。类型系统的切换不是信念更新；信念更新是在固定语义下调整真值。范式转移是改变语义本身。这类似于在编程里把一组 API 的返回类型从 Int 改成 String，所有调用点要么重新 typing，要么全局报错。

但类型论还提供了一个比 Kuhn 更精细的工具：coercion。相对论的“质量”在低速极限（v/c→0）下可以降级为牛顿质量，这叫“统制子”（coercion），而不是两个系统之间有翻译。后进理论可以说明为何旧理论在限定域内有效——因为存在一条从新类型到旧类型的可定义映射，在这个映射下，旧命题近似成立。这个映射是有方向性的、有适用域的。

问题：如果科学进步是一连串有向的 re-typing/coercion，那么科学实在论该拿什么做本体？是“最终所有类型都会被一个更大的类型系统统一”（强实在论），还是“我们只能追随 coercion 的路径，没有终点”（结构实在论）？请辩论。