In (an idealized version of) Haskell, is there a concrete type a
such that we can implement Eq a
lawfully, but it is impossible to implement Ord a
? The order doesn’t need to be meaningful, and any total order suffices, as long as it is implemented by a function that terminates and obeys the axioms.
This comes from the consideration that, to use certain efficient data structures such as Data.Set
, we must have a decidable total order. However sets can technically be implemented with Eq
alone, just that it becomes very inefficient. So is it possible to always implement Ord
? All the counterexamples I know of — Integer -> Bool
for example — can’t implement Eq
either. There is a likely candidate, though. The type (Integer -> Bool) -> Bool
, surprisingly, has computable Eq
, I’m still not sure whether Ord
is possible though.
I’m also interested in this question in other (non-contrived) type theories. There is indeed a type theory in which we have counterexamples: with nominal types, the atoms can be compared for equality but not order since everything is invariant under permutation of names by construction. What about MLTT? Or system F?