[m-dev.] [m-users.] Comparison in the reference manual

[Mark Brown]

On Mon, Nov 16, 2015 at 9:38 AM, Julien Fischer <jfischer at opturion.com> wrote:
>
> Hi Mark,
>
> On Mon, 16 Nov 2015, Mark Brown wrote:
>
>> Moved to developers list...

>> I'm wondering, can the language define a bit more than it has thus
>> far?
>
>
> I think that's a good idea; I suspect most users have been assuming more
> than that language actually guarantees anyway.

Attached diff is for review. Preferably by everyone, since it changes
the language and is a small diff.

The actual changes are still up for discussion.

>
>> The idea would be to provide some useful theorems, while being
>> careful not to constrain implementations too much. Here are some
>> suggestions:
>>
>> int: Define it as having the mathematical ordering, and require
>> implementations to disallow overflowing literals. The latter is so you
>> don't have 9223372036854775808 < 0 being true. (You may still have
>> 9223372036854775807 + 1 < 0, since the + operation is undefined on
>> overflow.)
>>
>> float: We can at least say that < and > never contradict the
>> mathematical ordering, even if = can due to lack of precision. Can we
>> assume implementations may use +/- infinity?
>
>
> If we are assuming IEEE 754 floats, yes.   For all of our current
> backends that is definitely yes.

For ints and floats I've decided to keep it conservative, and just say
that implementations are allowed to be inconsistent if literals are
out-of-range.

>
>> Otherwise a caveat on overflowing float literals may be needed.
>> (Incidentally, for an overflowing float literal I get an error from
>> the C compiler about infinity being undeclared.)
>
>
> Do you mean along the lines of bug #146?  (The intended fix is that
> the compiler should replace overflowing float literals with calls to
> float.infinity/0 or -float.infinity/0.)

Yes.

>
>> char: Are these officially unicode now?
>
>
> Yes.
>
>> We could define them as having the code point ordering.
>>
>> string: There are probably good reasons to keep this ordering
>> undefined. But maybe we could say something about the ascii subset?
>>
>> tuples: These exist as a convenience to the user. Would defining them
>> as having the obvious ordering be likely ever to cause problems for
>> implementations?
>
>
> No, I can't see that it would cause any problems.

Likewise for discriminated union types where both values have the same
principal constructor, I suppose. I've documented that too, but I'm
not so sure about that one. If anyone objects, please speak up.

Mark
-------------- next part --------------
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index f5c7e51..971f938 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -1932,6 +1932,7 @@ type classes (@pxref{Type classes}), and existentially quantified types
 * User-defined types::
 * Predicate and function type declarations::
 * Field access functions::
+* The standard ordering::
 @end menu
 
 @node Builtin types
@@ -2524,6 +2525,48 @@ update_field_in_map(Map, Index, Value) =
     Map ^ elem(Index) ^ field2 := Value.
 @end example
 
+ at node The standard ordering
+ at section The standard ordering
+
+For every Mercury type there exists a standard ordering;
+any two values of the same type can be compared under this ordering
+by using the @code{builtin.compare/3} predicate.
+The ordering is total, meaning that the corresponding binary relations
+are reflexive, transitive and anti-symmetric.
+
+The existence of this ordering makes it possible to implement
+generic data structures such as sets and maps,
+without needing to know the specifics of the ordering.
+Furthermore, different platforms often have their own natural orderings
+which are not necessarily consistent with each other.
+As such, the standard ordering for most types is undefined.
+
+For the builtin type @code{int},
+the standard ordering is the usual numerical ordering.
+Implementations are permitted to give inconsistent results
+for overflowing literals.
+
+For the builtin type @code{float},
+the standard ordering approximates the usual numerical ordering.
+If the result of @code{builtin.compare/3} is @code{(<)} or @code{(>)}
+then this relation holds in the numerical ordering,
+but this is not necessarily the case for @code{(=)} due to lack of precision.
+Implementations are permitted to give inconsistent results
+for overflowing literals.
+
+For the builtin type @code{char}, the standard ordering is
+the numerical ordering of the Unicode code point values.
+
+For tuple types, corresponding arguments are compared,
+with the first argument being the most significant.
+
+For discriminated union types,
+if both values have the same principal constructor
+then corresponding arguments are compared,
+with the first argument being the most significant.
+If the values have different principal constructors,
+the result of comparing them is not defined.
+
 @node Modes
 @chapter Modes