
The set of all values of the type is always enumerable (it's even recursive, since otherwise you wouldn't be able to tell if something is a value or not). Since it's enumerable, you can enumerate all values of that type: v1, v2, v3, ... Take x1 < x2 iff x1 precedes x2 in the above sequence. This is obviously computable. Roman On 01/01/15 17:31, Atze van der Ploeg wrote:
(That said, I don't understand why this discussion is relevant at all. The fact that the ordering exists doesn't mean that one would want to declare the Ord instance, like with complex numbers.)
It's not relevant, it's just an intellectual exercise.
For any set with a equality relation there exists a total order relation on that set consistent with the equality relation. The question is then whether there exists a set with a computable equality relation such that there is no computable total order.
I think the following computable function shows that it is always possible (it chooses an order during queries):
Maintain a table, initially emtpy
As soon as (a <= b) is requested, see if a and b are already in the table (using the computatble equality function) , if so, use their ordering in the table. If an element is not in the table, add it.
Hence the table gives a consistent total order (it depends on which ordering queries are requested, but that is not relevant?)
2015-01-01 16:06 GMT+01:00 Atze van der Ploeg
mailto:atzeus@gmail.com>: Nope you're right. Indeed uncompatible with the field structure. Now I'm confused :)
I now understand your question, but do not immediately know the answer. Anyone?
On Jan 1, 2015 4:02 PM, "Tom Ellis"
mailto:tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote: On Thu, Jan 01, 2015 at 03:52:26PM +0100, Atze van der Ploeg wrote: > If we do not require that (a <= b) && (a >= b) ==> a == b (where <= is > from the total ordering and == is from the equality relation) then it is > trivial, take the total ordering forall x y. x <= y that i mentioned > earlier. > > So the compatiblity with equality (you say field structure) is not besides > the point, in fact antisymmetry means that the ordering corresponds to the > equality relation. > > Clear now or did I misunderstand?
Here is my proposed equality and ordering on the complex numbers:
data Complex = Complex (Double, Double) deriving (Eq, Ord)
Does this violate any of my requested conditions? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe