包含 `Eq a` 但不包含 `Ord a` 的类型

Question

在Haskell（理想化版本）中，是否存在一个具体类型

a

，使得我们可以合法地实现

Eq a

，但又不可能实现

Ord a

？该顺序不需要有意义，任何全序就足够了，只要它是由终止并遵守公理的函数实现的。

这是出于这样的考虑：要使用某些高效的数据结构（例如

Data.Set

），我们必须有一个可判定的总顺序。然而，从技术上讲，集合可以单独使用

Eq

来实现，只是它变得非常低效。那么是否可以一直执行

Ord

呢？我所知道的所有反例 - 例如

Integer -> Bool

- 也无法实现

Eq

。

不过，有一个可能的候选人。类型

(Integer -> Bool) -> Bool

，令人惊讶的是，具有可计算的

Eq

。但对我来说，它似乎也具有可计算的

Ord

！由于模数（请参阅链接）是可计算的，因此我们可以首先按函数的模数对函数进行排序，然后在 2^n 个不同的输入前缀上比较两个函数，其中 n 是模数。

我也对其他（非人为的）类型理论中的这个问题感兴趣。确实存在一种类型理论，其中我们有反例：对于名义类型，可以比较原子的相等性，但不能比较顺序，因为在通过构造进行名称排列的情况下，一切都是不变的。 MLTT 怎么样？还是F系统？

Answer 1

我认为

IORef

是一个很好的候选人。您可以基于比较底层指针来实现一个实例，但这在运行之间并不稳定，尤其是在机器之间/体系结构之间，所以这似乎是一个坏主意。