理想Haskell中是否存在可合法实现Eq a却无法实现Ord a的类型？

核心结论 #

在理想化Haskell（基于全域纯λ演算，允许所有可计算函数）中，不存在这样的具体类型a：只要能合法实现符合要求的Eq a（即可判定、可终止的相等性检查），就一定能构造出满足全序公理的可终止Ord a。

关键分析 #

已知候选类型的排除 #

• Integer -> Bool：连Eq都无法实现——无法判定两个函数对所有整数输入的输出是否完全一致，因此不在讨论范围内。
• (Integer -> Bool) -> Bool：该类型确实具备可计算的Eq实现（基于“模数”概念：存在某个自然数n，函数的行为完全由输入函数在0到n-1上的取值决定）。同时，它也能实现合法的Ord：
  1. 先比较两个函数的模数，模数更小的函数排在前面；
  2. 若模数相同（设为n），枚举所有长度为n的整数前缀对应的输入函数组合，按字典序比较目标函数的输出结果，即可得到全序。

为什么不存在反例？ #

从可计算性理论的角度：

• 理想化Haskell中，所有能实现Eq a的类型a，其元素都是可计算对象，而可计算对象的编码是可数的。
• 对于可数且相等性可判定的集合，我们总能构造一个可计算的全序：比如将元素枚举为x₀, x₁, x₂, ...，定义x_i < x_j当且仅当i < j。这个序满足全序的所有公理，且是可终止、可判定的。

其他类型理论中的情况 #

带标称类型的理论 #

存在明确反例：比如原子名称类型，相等性可直接判定（比较名称是否为同一实体），但由于类型构造要求满足名称置换不变性，任何全序定义都会破坏这种对称性（比如指定某个名称为“最小”，置换后该名称的位置改变，序的结果也会变化），因此无法构造符合要求的Ord。

MLTT（Martin-Löf类型论） #

无论内涵还是外延MLTT，只要类型a具有可判定的相等性（即对任意x, y : a，能判定x ≡ y是否成立），就可以构造全序：

• 对归纳类型，可通过结构递归，基于子元素的序定义当前元素的序；
• 对函数类型，只有当定义域为有限类型时才具备可判定相等性，此时可枚举所有定义域元素的输出，按字典序定义函数的序。

System F #

System F中，若类型的项具有可判定的βη等价性（即Eq可实现），则同样能构造全序：

• 所有可定义项都可归约到规范形，规范形的结构是可数的；
• 基于规范形的结构（比如变量、抽象、应用的嵌套结构），可以定义字典序或枚举序，满足全序公理且可判定。

内容的提问来源于stack exchange，提问作者Trebor