A type with `Eq a` but not `Ord a`

Question

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. But to me it seems to also have computable Ord! Since the modulus (see the link) is computable, we can first order functions by their modulus, and then compare the two functions on their 2^n different input prefixes, where n is the modulus.

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?

Shiva

Currently, Complex a does not have an instance. It could have one, but not one that is compatible with its Num instance -- i.e. that has a < b && c < d => a+c < b+d. It was decided that this law is a sort of implicit assumption of most programmers, and could be a source of bugs if the Ord instance was made easily available. – Cb

Answer 1

I think IORef is a good candidate here. You could potentially implement an instance based on comparing the underlying pointers, but that isn't stable from run to run and especially from machine to machine/architecture to architecture, so it seems like a bad idea. I think the API doesn't even promise that the pointer stays the same over time within a single run -- e.g. garbage collection is likely permitted to move it, even if the current implementation doesn't do that.

Cb