<p>Many languages have some user-definable traits, interfaces or protocols with special status in the language's semantics or standard library, for which there is some kind of &quot;contract&quot; requiring that user-defined implementations satisfy certain mathematical properties for correctness. For example:</p>
<ul>
<li>User-defined <code>==</code> or <code>equals</code> is expected to be <a href="https://en.wikipedia.org/wiki/Reflexive_relation" rel="noreferrer">reflexive</a>, <a href="https://en.wikipedia.org/wiki/Symmetric_relation" rel="noreferrer">symmetric</a> and <a href="https://en.wikipedia.org/wiki/Transitive_relation" rel="noreferrer">transitive</a> (i.e. an <a href="https://en.wikipedia.org/wiki/Equivalence_relation" rel="noreferrer">equivalence relation</a>).</li>
<li>User-defined hash-codes are expected to be consistent with <code>==</code>/<code>equals</code>, and unchanging for the life of the object (even if the object is mutable).</li>
<li>User-defined ordering/comparisons are often expected to define a <a href="https://en.wikipedia.org/wiki/Total_order" rel="noreferrer">total order</a>.</li>
<li>Callback functions for some <code>fold</code>/<code>reduce</code> operations might be expected to define <a href="https://en.wikipedia.org/wiki/Associative_property" rel="noreferrer">associative</a> operations.</li>
</ul>
<p>However, it is infeasible or impossible in many real cases for a compiler to formally verify whether arbitrary user-defined code satisfies these contracts. So, what approaches do languages take to either enforce these rules, or otherwise ensure <a href="https://en.wikipedia.org/wiki/Memory_safety" rel="noreferrer">program safety</a> when the rules are violated?</p>
<hr />
<p><sup>Some languages may impose requirements on the asymptotic complexity of implementations of certain traits, e.g. a <a href="https://en.wikipedia.org/wiki/Set_(abstract_data_type)" rel="noreferrer">set</a> interface might require O(log <em>n</em>) membership tests. This question is only about requirements for program correctness, not requirements for performance.</sup></p>

<standard-library><traits><verification>
Approaches to enforcing contracts for standard user-definable traits
CC BY-SA 4.0
2023-08-04T16:10:50.363Z
A bit of a non-answer, but Swift "enforces" that `Equatable` and `Hashable` conformance match in debug builds by trapping at runtime when they disagree. AFAIK there's no such enforcement in release builds or at compile time.
Bbrk24
CC BY-SA 4.0
2023-08-04T16:19:09.830Z
Interesting, so far I have only used linters and tests to detect problems with `==`, hashcodes and total orders, but I'm curious if there are better approaches.
Eldritch Conundrum
CC BY-SA 4.0
2023-08-09T23:30:16.997Z
Just as a note, in IEEE-754 floating point, `NaN` is not equal to `NaN`. It is true that `x == x` holds for all floating point numbers `x`, but `NaN` is, by definition, not a number.
Pseudonym
CC BY-SA 4.0
2023-08-09T23:35:48.527Z
@Pseudonym Interesting case, but e.g. in Java despite the fact that `NaN == NaN` is false for the value type `double`, `new Double(NaN).equals(new Double(NaN))` is true for the boxed type ─ specifically [because of the `equals` contract](https://docs.oracle.com/en/java/javase/19/docs/api/java.base/java/lang/Double.html#equals(java.lang.Object)).
kaya3
CC BY-SA 4.0
2023-08-10T14:35:21.713Z
Note that the unchangedness of hash codes does not apply in Java for mutable objects
Seggan
<h1><a href="https://dlang.org/spec/contracts.html" rel="noreferrer">Contracts!</a></h1>
<p>You may already be aware of this, but <a href="https://en.wikipedia.org/wiki/Design_by_contract" rel="noreferrer"><strong>contracts</strong></a> have a formal meaning as requirements which are checked at runtime. For example, a function in a language like C or Java which throws an error if any of its arguments are <code>null</code>:</p>
<pre class="lang-java prettyprint-override"><code>BigNumber add(BigNumber a, BigNumber b) {
    // Contracts
    Objects.requireNonNull(a);
    Objects.requireNonNull(b);
    // Code
    ...
}
</code></pre>
<p>Of course pretty much any language supports the above. But <strong>some compilers have special support for contracts, which removes validation code for arguments which trivially satisfy their contracts, fails at compile-time for arguments which trivially violate them, and refines the arguments' types after their contracts with the knowledge that if they failed, control flow would divert elsewhere</strong>; exactly the things you're looking for.</p>
<h2>How are contracts checked?</h2>
<p><strong>Generally, contracts are checked at compile-time with <a href="https://en.wikipedia.org/wiki/Flow-sensitive_typing" rel="noreferrer">flow-sensitive typing</a> and a limited form of <a href="https://en.wikipedia.org/wiki/Refinement_type" rel="noreferrer">refinement types</a></strong>. Basically, the compiler holds on to every predicate a value is guaranteed to satisfy at compile time, as it passes through control flow and picks up new predicates via if-conditions and other contracts. For example, in</p>
<pre class="lang-java prettyprint-override"><code>BigNumber weight(BigNumber a, BigNumber b) {
    Objects.requireNonNull(a);
    Objects.requireNonNull(b);
    assert(!a.isNegative() &amp;&amp; !b.isNegative());
    if (a.isZero() &amp;&amp; b.isZero()) {
        return 0;
    }
    
    return divide(a, add(a, b));
}
</code></pre>
<p>a smart compiler would infer that the arguments to <code>divide</code> and <code>add</code> are non-null, and a <em>really</em> smart compiler would infer that the second argument to <code>divide</code> is non-zero, and elide all of the contracts.</p>
<h3>Challenges</h3>
<p>Be aware that checking more complex cases is <em>hard</em> (most compilers probably wouldn't even infer that <code>divide</code>'s second argument is non-zero). I've looked at <a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="noreferrer">Liquid Haskell</a> which has refinement types (very similar to contracts but always resolved at compile-time), and it's rarely used for anything more than basic examples which lend themselves well to structural recursion and proofs. Even you look at the <a href="https://liquid.kosmikus.org/01-intro.html" rel="noreferrer">tutorial</a> or <a href="https://ucsd-progsys.github.io/liquidhaskell-tutorial/" rel="noreferrer">this one</a>, it gets <a href="https://liquid.kosmikus.org/04-proofs.html" rel="noreferrer"><em>really</em> complicated</a> <a href="https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_08_Measure_Set.html" rel="noreferrer"><em>really</em> fast</a>, with lots of extra and unintuitive annotations for things like measure functions (and these examples are still inductive).</p>
<p>This is why you don't see contracts much; the cost of validation is usually really high, and the number of cases you can skip validation are usually really low.</p>
<h2>Examples in real compilers</h2>
<p>See <a href="https://en.wikipedia.org/wiki/Design_by_contract#Language_support" rel="noreferrer">here (Wikipedia)</a> for all currently-known implementations of contract programming, of which there are many. Although, many of these don't provide compile-time validation and elision of trivial cases (a smart compiler can elide trivial contracts in some cases, but not others like those in non-inlined functions). Notable examples:</p>
<ul>
<li><p><a href="https://docs.racket-lang.org/reference/contracts.html" rel="noreferrer">Contracts in Racket</a>. Racket has had contracts for a long time, and they are built into the standard library (e.g. most predicates like <code>symbol?</code>, which check a value's type, double as contracts which will assert to the compiler that the value is the correct type in the true branch). Racket supports many different kinds of contracts, such as <a href="https://docs.racket-lang.org/reference/collapsible.html" rel="noreferrer">collapsible contracts</a> (to reduce validation time), <a href="https://docs.racket-lang.org/reference/chaperones.html" rel="noreferrer">impersonator and chaperone contracts</a> (I don't fully understand), and <a href="https://docs.racket-lang.org/reference/Building_New_Contract_Combinators.html" rel="noreferrer">contract combinators</a> (warning: the first function here is <em>huge</em>. These are simply functions which take a contract and return another one)</p>
</li>
<li><p>Kotlin has <a href="https://kotlinlang.org/api/latest/jvm/stdlib/kotlin.contracts/" rel="noreferrer">experimental contracts</a>, see <a href="https://github.com/Kotlin/KEEP/blob/master/proposals/kotlin-contracts.md" rel="noreferrer">the proposal</a> and <a href="https://stackoverflow.com/questions/60958843/what-is-the-purpose-of-kotlin-contract">SO post</a>. Kotlin already has <a href="https://kotlinlang.org/spec/type-inference.html#smart-casts" rel="noreferrer">flow-sensitive typing</a> (i.e. if you check that a value has a specific type with a predicate like <code>is</code>, in an <code>if</code> or <code>when</code> statement, the true branch of that statement will let you use the value as if it were the checked type without casting), and flow-sensitivity / contracts help one another; functions which return predicates based on a type implementing specific guarantees are useful in both contracts (for asserting such guarantees) and flow-sensitive <code>if</code> conditions (for simply checking them).</p>
</li>
<li><p><a href="https://dlang.org/articles/cppcontracts.html" rel="noreferrer">D has an article on why its contracts are better than simple C++ assertions</a>. Which shows that contracts are more than just assertions, even without compile-time validation and elision (which AFAIK D doesn't have).</p>
</li>
<li><p><a href="https://projectlombok.org/features/NonNull" rel="noreferrer"><code>@NonNull</code> in Lombok</a> (though <a href="https://stackoverflow.com/a/13485074">not every <code>@NonNull</code> annotation</a> is actually checked, Lombok's is). The above function can be re-written in this way, which will prevent you from trivially passing <code>null</code> at compile-time, and hint to the compiler and IDE that the return value is non-null:</p>
</li>
</ul>
<pre class="lang-java prettyprint-override"><code>@NonNull BigNumber add(@NonNull BigNumber a, @NonNull BigNumber b) {
    ...
}
</code></pre>

CC BY-SA 4.0
2023-08-05T21:26:41.833Z
2023-08-05T21:47:17.093Z
2023-08-05T21:47:17.093Z
tarzh
CC BY-SA 4.0
2023-08-05T21:44:27.650Z
To be clear, is `BigNumber` unsigned? Otherwise I don't see how it follows that `add(a, b)` is nonzero.
kaya3
CC BY-SA 4.0
2023-08-05T21:45:32.060Z
Good catch, I was assuming so
tarzh
<h2>Allow implementing eq/cmp only in terms of conversion standard types</h2>
<p><em>this applies only really to ==, &gt;, &lt;. It can encourage proper hash functions too but not enforce it</em></p>
<p>In general, enforcing if arbitrary code produces a total ordering or is symmetric is incomputable. However, if, instead of returning a comparison, you provide a standard way to allow objects to be converted to some primitive for the purpose of comparison, and you know that primitive is reflexive, symetric etc.</p>
<p>For example, in a traditional language you might write:</p>
<pre><code>class A {
    int field; 

   public cmp(A other) {return this.field - other.field;}
}
</code></pre>
<p>But now, in the new version you would need to:</p>
<pre><code>class A {
    int field;
    public getCmpKey() {return this.field; }
}
</code></pre>
<p>Since you know arrays and tuples are totally ordered and transitive you can easily implement comparison by multiple fields:</p>
<pre><code>class A {
    int fieldA;
    int fieldB;
    Array&lt;A&gt; fieldC;
    
    public getCmpKey() {
        return (fieldA, fieldB, fieldC);
    }
}
</code></pre>
<p>Or if you, for example, want to compare strings according in some custom order you could do:</p>
<pre><code>class A {
    string field;
    
    public getCmpKey() {
        return this.field.map((i)=&gt;&quot;zZkKdDbB&quot;.index(i).or_else(i.ord()+6));
    }
}
</code></pre>
<p>This has a lot of advantages:</p>
<ul>
<li>Typically, when implementing equality or inequality operators, you <em>want</em> to just check if a group of fields match. Simply returning the fields is much more convenient than needing to check them all one by one.</li>
<li>You can guarantee symmetry , reflexivity, and transitivity.</li>
</ul>
<p>However, there are some downsides:</p>
<ul>
<li>You are limited in the types of comparisons you can represent</li>
<li>Some operations that might be easy to represent using a simple cmp function become hard. Things like advanced unicode collations</li>
<li>There can be a performance cost. Since you need to output all fields at once you can't return early and skip computing later tiebreakers in comparison operators when one of the earlier ones already returns non-equal.</li>
</ul>
<h3>Hashes</h3>
<p>For hashes, this won't do anything to ensure the hashes won't change since you are free to return a random value each time. However, they may still have the benefit of making implementing a hash function much easier and conciser.</p>
<p>It can also encourage hash to match <code>==</code> but since the object returned can change each time it can change between using the hash and <code>==</code></p>

CC BY-SA 4.0
2023-08-04T16:27:44.770Z
2023-08-04T16:35:52.660Z
2023-08-04T16:35:52.660Z
mousetail 'he-him'
CC BY-SA 4.0
2023-08-04T16:32:48.197Z
The last point about performance cost might be avoided if `getCmpKey` can be inlined where it's called.
kaya3
CC BY-SA 4.0
2023-08-04T16:40:13.090Z
This answer would be improved by citing some existing languages that implement things this way.
Alexis King
CC BY-SA 4.0
2023-08-04T16:52:53.607Z
This might solve the particular case of comparisons, but what about things like [`count`](https://developer.apple.com/documentation/swift/collection/count-4l4qk) (O(n)) and [`underestimatedCount`](https://developer.apple.com/documentation/swift/sequence/underestimatedcount-3afwr) (O(1), no greater than actual count)? Or any set of operations defined in user code rather than the compiler?
Bbrk24
CC BY-SA 4.0
2023-08-04T16:58:44.297Z
@Bbrk24 I specifically state this would only work for comparisons
mousetail 'he-him'
CC BY-SA 4.0
2023-08-04T20:29:58.930Z
This reminds me of how Python supports custom sorting. In most languages you provide a comparison function, but in Python you provide a key-extraction function and it then uses the built-in comparison function on this.
Barmar
CC BY-SA 4.0
2023-08-05T23:12:28.397Z
This would create a lot of issues for things like custom bigint or rational types. E.g., if the language only has ints and floats, you have no way to compare bigints (well, perhaps with the exception of converting to a string and relying on lexicographic comparison?). And even with bigint support, that falls apart with rationals.
rydwolf
CC BY-SA 4.0
2023-08-06T05:15:22.927Z
@RydwolfPrograms Bigints can be trivially converted into arrays that preserve sort order. Rationals are a bit harder
mousetail 'he-him'
CC BY-SA 4.0
2023-08-06T05:20:52.637Z
@RydwolfPrograms Rationals can be done too, you can represent them as the sum of a list of numbers divided by consecutive primes. This would preserve sort order
mousetail 'he-him'
CC BY-SA 4.0
2023-08-08T14:34:14.103Z
@mousetail I don't think that is right. If you convert the bigint `23` to an array you get `[2, 3]` and if you convert `111` you get `[1, 1, 1]`, which is lexicographically smaller. And you can't convert `23` to `[0, 2, 3]` because you don't know how many digits it's going to have to be compared with.
kaya3
CC BY-SA 4.0
2023-08-08T14:38:21.317Z
On the other hand, a `getCmpKey` for rational numbers can be implemented by finding the continued fraction representation as an array, then flipping the signs of alternating terms ─ [the resulting arrays for two rational numbers can be compared lexicographically](https://perl.plover.com/classes/cftalk/TALK/slide044.html), assuming you can compare the integers in the arrays of course.
kaya3
CC BY-SA 4.0
2023-08-08T14:49:13.967Z
@kaya3-supportthestrike You can encode every digit into a `[index, digit]` tuple and it will maintain sort order
mousetail 'he-him'
<p><em>Note: similar to @mousetail's <a href="https://langdev.stackexchange.com/a/2659/874">answer</a>, with references.</em></p>
<h3>Hashing in Rust</h3>
<p>One of the key innovations of the Rust standard library was <em>hashing</em>.</p>
<p>In contemporary main stream languages such as C++<sup>1</sup> or Java, a hash function for a value returns its hash:</p>
<pre class="lang-java prettyprint-override"><code>@Override
public int hashCode() {
    return (int) id * name.hashCode() * email.hashCode();
}
</code></pre>
<p>The key problem with this approach is that the actual hash algorithm is <em>hardcoded</em>, and often -- for the sake of simplicity -- of poor quality.</p>
<p>Instead, in Rust, the &quot;equivalent&quot; code is:</p>
<pre class="lang-rust prettyprint-override"><code>impl Hash for MyStuff {
    fn hash&lt;H: Hasher&gt;(&amp;self, mut hasher: H) {
        hasher.hash(self.id);
        hasher.hash(self.name);
        hasher.hash(self.email);
    }
}
</code></pre>
<p>That is, the user-code is separated in two:</p>
<ol>
<li>The <code>Hash</code> implementation provides <em>which fields to hash</em>.</li>
<li>The <code>Hasher</code> implementation provides <em>how to hash</em>.</li>
</ol>
<p>Much cleaner (SRP) and easier (at equal quality).</p>
<p><sup>1</sup> <em>Howard Hinnant made a proposal for a similar hash framework for C++ (see <a href="http://htmlpreview.github.io/?https://github.com/HowardHinnant/papers/blob/master/hashing.html" rel="nofollow noreferrer">D3890: Types Don't Know #</a>) but unfortunately it didn't fly.</em></p>
<h3>Rust it!</h3>
<p>The key innovation of separating the identification of the fields defining the identity of the value from doing something with those fields would allow ensuring that equality and ordering are <em>also</em> properly defined.</p>
<p>It does get <em>trickier</em>, admittedly:</p>
<ol>
<li>The concept must be applied to two values.</li>
<li>Ideally, with short-circuiting.</li>
</ol>
<p><em>Both</em> of those issues can be solved by using a <em>coroutine</em> implementation. In a dynamically typed language, the coroutine can simply yield its values, one at a time. In a statically typed language, it's easier if the coroutine instead passes each field to an argument, in turn.</p>
<p>Furthermore, the use of Affine Types can ensure that the coroutine <em>cannot</em> pass multiple fields consecutively without yielding, to prevent erroneous implementations.</p>
<p>As a <em>sketch</em><sup>2</sup> the implementation in Rust would look something like that:</p>
<pre class="lang-rust prettyprint-override"><code>impl Identity for MyStuff {
    gen fn identity&lt;R: Runner&gt;(&amp;self, runner: R) -&gt; R::Done {
        let runner = yield runner.next(self.id).await;
        let runner = yield runner.next(self.name).await;
        let runner = yield runner.next(self.email).await;

        runner.done()
    }
}
</code></pre>
<p>A runner implementation for equality would then perform a <em>ping pong</em> between the two values, taking one item at a time from each, and comparing them.</p>
<p>The main advantage compared to @mousetail's approach is purely one of implementation -- namely, allowing short-circuiting. The core message -- separating identifying the fields from computing the result -- is similar.</p>
<p><sup>2</sup> <em>Rust doesn't quite have support for &quot;generators&quot;, right now... so I need to improvise a bit.</em></p>

CC BY-SA 4.0
2023-08-08T11:47:43.970Z
2023-08-08T11:47:43.970Z
Matthieu M.
CC BY-SA 4.0
2023-08-08T15:16:41.577Z
Swift does the same thing with its `Hashable` protocol since 4.2 ([proposal](https://github.com/apple/swift-evolution/blob/main/proposals/0206-hashable-enhancements.md)), and there's no doubt in my mind that between Swift and Rust one design heavily influenced the other.
Bbrk24
CC BY-SA 4.0
2023-08-08T15:18:34.373Z
@Bbrk24: I expect Swift stole that one from Rust, maybe in retaliation for Rust stealing `if let` and `while let` :)
Matthieu M.
CC BY-SA 4.0
2023-08-08T15:24:11.543Z
Swift has taken quite a few things from Rust -- off the top of my head, the keywords `some` and `any` are ripped directly from `impl` and `dyn` respectively, and `Sendable` is named after Rust's `Send` (though `Sendable` goes farther, and AIUI is equivalent to `Sync`).
Bbrk24
CC BY-SA 4.0
2023-08-08T15:27:00.967Z
I don't use Rust though, so my understanding of a number of Rust's features is only via the Swift equivalent :^)
Bbrk24
CC BY-SA 4.0
2023-08-08T16:08:51.747Z
@Bbrk24: Swift also took a number of Rust developers, starting with Graydon Hoare, its creator :P I do like to see this cross-pollination, the most sincere form of flattery being imitation, as they say.
Matthieu M.
CC BY-SA 4.0
2023-08-10T14:40:56.080Z
Note that Java has something similar to Rust with Objects.hash and Objects.hashCode
Seggan
CC BY-SA 4.0
2023-08-10T15:18:55.373Z
@Seggan: Is there a way to customize the hashing algorithm is Java? It seems hardcoded to... whatever the JVM you're using thinks is suitable.
Matthieu M.
CC BY-SA 4.0
2023-08-10T16:57:29.557Z
@MatthieuM. indeed it is not, just pointing out the same "constructible hashcode" thing
Seggan
<h1>Don't enforce, expose <em>to</em> derive it</h1>
<p>As you noted, it is infeasible to impossible for a compiler to formally verify general user code. The difficulty arises because the implementation of these standard traits are <em>encapsulated away</em> in implementation methods. It is hard to verify general code, but it is not necessary to verify these cases if you generate them.</p>
<h2>Equals</h2>
<p><code>==</code> or <code>.equals()</code> methods are generally implemented by inspecting internal properties for equality, short circuiting on the first fail. Code like this:</p>
<pre class="lang-cs prettyprint-override"><code>def equals(Object other) as bool
{
    if ( other is Type.Of( this ) )
    {
        if ( propOne != other.propOne ) return false;
        if ( propTwo != other.propTwo ) return false;
        return true;
    }
    return false;
}
</code></pre>
<p>This is tedious to write, but it is very easy to do <em>contract correct derive it</em>, if the relevant internal properties are annotated for this.</p>
<p>Something like:</p>
<pre class="lang-cs prettyprint-override"><code>#[derive(Eq(propOne,propTwo)]
class X
{
    var propOne as TypeX
    var propTwo as TypeY
    var otherNotIdentifingProp as UnsafePointer
}
</code></pre>
<p>So the compiler can both generate <em>and</em> validade that each element within the <code>==</code> chain has a valid equals implementation.</p>
<p>User defined implementations of equals should be possible, but discouraged:</p>
<pre class="lang-cs prettyprint-override"><code>unsafe def [Eq] (Object other) as bool { return rand() % 3; }
</code></pre>
<h2>Hashs</h2>
<p>User defined hashcodes have almost the same properties as the user defined equality, with the extra requisites that it should be consistent (same hash if two objects compare equal) and be stable (do not change before invocations).</p>
<p>So (the only?) way to solve this is by deriving it in tandem with any user-defined <code>==</code> derivation.</p>
<pre class="lang-cs prettyprint-override"><code>#[derive(Eq(propOne,propTwo),Hasher]
class X
{
    //Hasher only exists paired with Eq
}
</code></pre>
<p>But I would argue that hashing is not a special contract in the language's semantics, but a normal contract <em>for the language's collections library</em>, and because of that, it should be a interface on collection namespace. Something like</p>
<pre class="lang-cs prettyprint-override"><code>interface HasherInterface
{
    private HashCode( Hasher hasher ) as u32
    {
        // Hasher as parameter to facilitate by collection hashing algorithm,
        // and because oCERT-2011-003 will haunt us forever
        // http://ocert.org/advisories/ocert-2011-003.html
    }
}
</code></pre>
<p>Because of its special relation with equality, any class automatically derived with <code>Ed,Hasher</code> should automatically implement <code>HasherInterface</code> too, and direct implementation of <code>HasherInterface</code> should be discouraged as unsafe.</p>
<p>Having a separate, opt-in interface for stable hashing is the first step to avoid silently bugs, and it is an extra reason for <a href="https://langdev.stackexchange.com/questions/2153/what-are-the-advantages-disadvantages-of-making-every-class-an-instance-of-an-ob/2169#2169">not</a> having methods in top types, so only capable objects expose this capacity.</p>
<h2>Ord</h2>
<p>Ordering is easy, but separated from equality or hashing, for <code>SortedList</code>/<code>SortedDict</code> collections:</p>
<pre class="lang-cs prettyprint-override"><code>// DTO value type, all fields mutating. Eq, but not Hasher

struct Signal
{
    var date as DateTime;
    var observed as int;

    def derive Eq(observed);
    def derive Ord(date);
}

// DTO reference type, all fields mutating. Not Eq or Hasher, but Ord

class Person
{
    var id as int;             // pk, db generated (mutating)
    var firstName as string;
    var lastName as string;

    def derive Eq(id), Hasher; // compiler error
    def derive Ord(id)         // default implementation for sorted collections

    // DRY: auto generate common OrdBy$name to avoid repetitions
    // also, guarantees total order in this cases.

    def derive OrdBy(&quot;LastFirst&quot;, lastName, firstName);
    def derive OrdBy(&quot;FirstLast&quot;, firstName, lastName);

    // var list1 = new SortedList&lt;Person&gt;();
    // var list2 = new SortedList&lt;Person.OrdByLastFirst&gt;();

}
</code></pre>

CC BY-SA 4.0
2023-08-09T16:13:37.393Z
2023-08-10T22:04:48.393Z
2023-08-10T22:04:48.393Z
André L F S Bacci
CC BY-SA 4.0
2023-08-09T18:45:52.227Z
Indeed, hashing is normally only used in some collection types in the standard library. However, if it could be enforced that hashes are stable and consistent with equals, then hashes could be cached, and the `==` operator could plausibly compare hashes as a shortcut for equality of complex nested objects.
kaya3
# Approaches to enforcing contracts for standard user-definable traits
Posted by: username_0 on 2023-08-04
Many languages have some user-definable traits, interfaces or protocols with special status in the language's semantics or standard library, for which there is some kind of "contract" requiring that user-defined implementations satisfy certain mathematical properties for correctness. For example:

* User-defined `==` or `equals` is expected to be [reflexive](https://en.wikipedia.org/wiki/Reflexive_relation), [symmetric](https://en.wikipedia.org/wiki/Symmetric_relation) and [transitive](https://en.wikipedia.org/wiki/Transitive_relation) (i.e. an [equivalence relation](https://en.wikipedia.org/wiki/Equivalence_relation)).
* User-defined hash-codes are expected to be consistent with `==`/`equals`, and unchanging for the life of the object (even if the object is mutable).
* User-defined ordering/comparisons are often expected to define a [total order](https://en.wikipedia.org/wiki/Total_order).
* Callback functions for some `fold`/`reduce` operations might be expected to define [associative](https://en.wikipedia.org/wiki/Associative_property) operations.

However, it is infeasible or impossible in many real cases for a compiler to formally verify whether arbitrary user-defined code satisfies these contracts. So, what approaches do languages take to either enforce these rules, or otherwise ensure [program safety](https://en.wikipedia.org/wiki/Memory_safety) when the rules are violated?

---

Some languages may impose requirements on the asymptotic complexity of implementations of certain traits, e.g. a [set](https://en.wikipedia.org/wiki/Set_(abstract_data_type)) interface might require O(log *n*) membership tests. This question is only about requirements for program correctness, not requirements for performance.
**Tags:** standard-library traits verification
> **Comments:**
> **username_1**: A bit of a non-answer, but Swift "enforces" that `Equatable` and `Hashable` conformance match in debug builds by trapping at runtime when they disagree. AFAIK there's no such enforcement in release builds or at compile time.  
> **username_2**: Interesting, so far I have only used linters and tests to detect problems with `==`, hashcodes and total orders, but I'm curious if there are better approaches.  
> **username_3**: Just as a note, in IEEE-754 floating point, `NaN` is not equal to `NaN`. It is true that `x == x` holds for all floating point numbers `x`, but `NaN` is, by definition, not a number.  
> **username_0**: @Pseudonym Interesting case, but e.g. in Java despite the fact that `NaN == NaN` is false for the value type `double`, `new Double(NaN).equals(new Double(NaN))` is true for the boxed type ─ specifically [because of the `equals` contract](https://docs.oracle.com/en/java/javase/19/docs/api/java.base/java/lang/Double.html#equals(java.lang.Object)).  
> **username_4**: Note that the unchangedness of hash codes does not apply in Java for mutable objects  
---
## 4 answers
### Answer by username_5 on 2023-08-05. Score: 7
Contracts!
You may already be aware of this, but contracts have a formal meaning as requirements which are checked at runtime. For example, a function in a language like C or Java which throws an error if any of its arguments are null:
BigNumber add(BigNumber a, BigNumber b) {
    // Contracts
    Objects.requireNonNull(a);
    Objects.requireNonNull(b);
    // Code
    ...
}

Of course pretty much any language supports the above. But some compilers have special support for contracts, which removes validation code for arguments which trivially satisfy their contracts, fails at compile-time for arguments which trivially violate them, and refines the arguments' types after their contracts with the knowledge that if they failed, control flow would divert elsewhere; exactly the things you're looking for.
How are contracts checked?
Generally, contracts are checked at compile-time with flow-sensitive typing and a limited form of refinement types. Basically, the compiler holds on to every predicate a value is guaranteed to satisfy at compile time, as it passes through control flow and picks up new predicates via if-conditions and other contracts. For example, in
BigNumber weight(BigNumber a, BigNumber b) {
    Objects.requireNonNull(a);
    Objects.requireNonNull(b);
    assert(!a.isNegative() && !b.isNegative());
    if (a.isZero() && b.isZero()) {
        return 0;
    }
    
    return divide(a, add(a, b));
}

a smart compiler would infer that the arguments to divide and add are non-null, and a really smart compiler would infer that the second argument to divide is non-zero, and elide all of the contracts.
Challenges
Be aware that checking more complex cases is hard (most compilers probably wouldn't even infer that divide's second argument is non-zero). I've looked at Liquid Haskell which has refinement types (very similar to contracts but always resolved at compile-time), and it's rarely used for anything more than basic examples which lend themselves well to structural recursion and proofs. Even you look at the tutorial or this one, it gets really complicated really fast, with lots of extra and unintuitive annotations for things like measure functions (and these examples are still inductive).
This is why you don't see contracts much; the cost of validation is usually really high, and the number of cases you can skip validation are usually really low.
Examples in real compilers
See here (Wikipedia) for all currently-known implementations of contract programming, of which there are many. Although, many of these don't provide compile-time validation and elision of trivial cases (a smart compiler can elide trivial contracts in some cases, but not others like those in non-inlined functions). Notable examples:

Contracts in Racket. Racket has had contracts for a long time, and they are built into the standard library (e.g. most predicates like symbol?, which check a value's type, double as contracts which will assert to the compiler that the value is the correct type in the true branch). Racket supports many different kinds of contracts, such as collapsible contracts (to reduce validation time), impersonator and chaperone contracts (I don't fully understand), and contract combinators (warning: the first function here is huge. These are simply functions which take a contract and return another one)

Kotlin has experimental contracts, see the proposal and SO post. Kotlin already has flow-sensitive typing (i.e. if you check that a value has a specific type with a predicate like is, in an if or when statement, the true branch of that statement will let you use the value as if it were the checked type without casting), and flow-sensitivity / contracts help one another; functions which return predicates based on a type implementing specific guarantees are useful in both contracts (for asserting such guarantees) and flow-sensitive if conditions (for simply checking them).

D has an article on why its contracts are better than simple C++ assertions. Which shows that contracts are more than just assertions, even without compile-time validation and elision (which AFAIK D doesn't have).

@NonNull in Lombok (though not every @NonNull annotation is actually checked, Lombok's is). The above function can be re-written in this way, which will prevent you from trivially passing null at compile-time, and hint to the compiler and IDE that the return value is non-null:


@NonNull BigNumber add(@NonNull BigNumber a, @NonNull BigNumber b) {
    ...
}
> **Comments:**
> **username_0** (2023-08-05): To be clear, is `BigNumber` unsigned? Otherwise I don't see how it follows that `add(a, b)` is nonzero.  
> **username_5** (2023-08-05): Good catch, I was assuming so  
---
### Answer by username_6 on 2023-08-04. Score: 4
Allow implementing eq/cmp only in terms of conversion standard types
this applies only really to ==, >, <. It can encourage proper hash functions too but not enforce it
In general, enforcing if arbitrary code produces a total ordering or is symmetric is incomputable. However, if, instead of returning a comparison, you provide a standard way to allow objects to be converted to some primitive for the purpose of comparison, and you know that primitive is reflexive, symetric etc.
For example, in a traditional language you might write:
class A {
    int field; 

   public cmp(A other) {return this.field - other.field;}
}

But now, in the new version you would need to:
class A {
    int field;
    public getCmpKey() {return this.field; }
}

Since you know arrays and tuples are totally ordered and transitive you can easily implement comparison by multiple fields:
class A {
    int fieldA;
    int fieldB;
    Array fieldC;
    
    public getCmpKey() {
        return (fieldA, fieldB, fieldC);
    }
}

Or if you, for example, want to compare strings according in some custom order you could do:
class A {
    string field;
    
    public getCmpKey() {
        return this.field.map((i)=>"zZkKdDbB".index(i).or_else(i.ord()+6));
    }
}

This has a lot of advantages:

Typically, when implementing equality or inequality operators, you want to just check if a group of fields match. Simply returning the fields is much more convenient than needing to check them all one by one.
You can guarantee symmetry , reflexivity, and transitivity.

However, there are some downsides:

You are limited in the types of comparisons you can represent
Some operations that might be easy to represent using a simple cmp function become hard. Things like advanced unicode collations
There can be a performance cost. Since you need to output all fields at once you can't return early and skip computing later tiebreakers in comparison operators when one of the earlier ones already returns non-equal.

Hashes
For hashes, this won't do anything to ensure the hashes won't change since you are free to return a random value each time. However, they may still have the benefit of making implementing a hash function much easier and conciser.
It can also encourage hash to match == but since the object returned can change each time it can change between using the hash and ==
> **Comments:**
> **username_0** (2023-08-04): The last point about performance cost might be avoided if `getCmpKey` can be inlined where it's called.  
> **username_7** (2023-08-04): This answer would be improved by citing some existing languages that implement things this way.  
> **username_1** (2023-08-04): This might solve the particular case of comparisons, but what about things like [`count`](https://developer.apple.com/documentation/swift/collection/count-4l4qk) (O(n)) and [`underestimatedCount`](https://developer.apple.com/documentation/swift/sequence/underestimatedcount-3afwr) (O(1), no greater than actual count)? Or any set of operations defined in user code rather than the compiler?  
> **username_6** (2023-08-04): @Bbrk24 I specifically state this would only work for comparisons  
> **username_8** (2023-08-04): This reminds me of how Python supports custom sorting. In most languages you provide a comparison function, but in Python you provide a key-extraction function and it then uses the built-in comparison function on this.  
> **username_9** (2023-08-05): This would create a lot of issues for things like custom bigint or rational types. E.g., if the language only has ints and floats, you have no way to compare bigints (well, perhaps with the exception of converting to a string and relying on lexicographic comparison?). And even with bigint support, that falls apart with rationals.  
> **username_6** (2023-08-06): @RydwolfPrograms Bigints can be trivially converted into arrays that preserve sort order. Rationals are a bit harder  
> **username_6** (2023-08-06): @RydwolfPrograms Rationals can be done too, you can represent them as the sum of a list of numbers divided by consecutive primes. This would preserve sort order  
> **username_0** (2023-08-08): @mousetail I don't think that is right. If you convert the bigint `23` to an array you get `[2, 3]` and if you convert `111` you get `[1, 1, 1]`, which is lexicographically smaller. And you can't convert `23` to `[0, 2, 3]` because you don't know how many digits it's going to have to be compared with.  
> **username_0** (2023-08-08): On the other hand, a `getCmpKey` for rational numbers can be implemented by finding the continued fraction representation as an array, then flipping the signs of alternating terms ─ [the resulting arrays for two rational numbers can be compared lexicographically](https://perl.plover.com/classes/cftalk/TALK/slide044.html), assuming you can compare the integers in the arrays of course.  
> **username_6** (2023-08-08): @kaya3-supportthestrike You can encode every digit into a `[index, digit]` tuple and it will maintain sort order  
---
### Answer by username_10 on 2023-08-08. Score: 4
Note: similar to @mousetail's answer, with references.
Hashing in Rust
One of the key innovations of the Rust standard library was hashing.
In contemporary main stream languages such as C++1 or Java, a hash function for a value returns its hash:
@Override
public int hashCode() {
    return (int) id * name.hashCode() * email.hashCode();
}

The key problem with this approach is that the actual hash algorithm is hardcoded, and often -- for the sake of simplicity -- of poor quality.
Instead, in Rust, the "equivalent" code is:
impl Hash for MyStuff {
    fn hash(&self, mut hasher: H) {
        hasher.hash(self.id);
        hasher.hash(self.name);
        hasher.hash(self.email);
    }
}

That is, the user-code is separated in two:

The Hash implementation provides which fields to hash.
The Hasher implementation provides how to hash.

Much cleaner (SRP) and easier (at equal quality).
1 Howard Hinnant made a proposal for a similar hash framework for C++ (see D3890: Types Don't Know #) but unfortunately it didn't fly.
Rust it!
The key innovation of separating the identification of the fields defining the identity of the value from doing something with those fields would allow ensuring that equality and ordering are also properly defined.
It does get trickier, admittedly:

The concept must be applied to two values.
Ideally, with short-circuiting.

Both of those issues can be solved by using a coroutine implementation. In a dynamically typed language, the coroutine can simply yield its values, one at a time. In a statically typed language, it's easier if the coroutine instead passes each field to an argument, in turn.
Furthermore, the use of Affine Types can ensure that the coroutine cannot pass multiple fields consecutively without yielding, to prevent erroneous implementations.
As a sketch2 the implementation in Rust would look something like that:
impl Identity for MyStuff {
    gen fn identity(&self, runner: R) -> R::Done {
        let runner = yield runner.next(self.id).await;
        let runner = yield runner.next(self.name).await;
        let runner = yield runner.next(self.email).await;

        runner.done()
    }
}

A runner implementation for equality would then perform a ping pong between the two values, taking one item at a time from each, and comparing them.
The main advantage compared to @mousetail's approach is purely one of implementation -- namely, allowing short-circuiting. The core message -- separating identifying the fields from computing the result -- is similar.
2 Rust doesn't quite have support for "generators", right now... so I need to improvise a bit.
> **Comments:**
> **username_1** (2023-08-08): Swift does the same thing with its `Hashable` protocol since 4.2 ([proposal](https://github.com/apple/swift-evolution/blob/main/proposals/0206-hashable-enhancements.md)), and there's no doubt in my mind that between Swift and Rust one design heavily influenced the other.  
> **username_10** (2023-08-08): @Bbrk24: I expect Swift stole that one from Rust, maybe in retaliation for Rust stealing `if let` and `while let` :)  
> **username_1** (2023-08-08): Swift has taken quite a few things from Rust -- off the top of my head, the keywords `some` and `any` are ripped directly from `impl` and `dyn` respectively, and `Sendable` is named after Rust's `Send` (though `Sendable` goes farther, and AIUI is equivalent to `Sync`).  
> **username_1** (2023-08-08): I don't use Rust though, so my understanding of a number of Rust's features is only via the Swift equivalent :^)  
> **username_10** (2023-08-08): @Bbrk24: Swift also took a number of Rust developers, starting with Graydon Hoare, its creator :P I do like to see this cross-pollination, the most sincere form of flattery being imitation, as they say.  
> **username_4** (2023-08-10): Note that Java has something similar to Rust with Objects.hash and Objects.hashCode  
> **username_10** (2023-08-10): @Seggan: Is there a way to customize the hashing algorithm is Java? It seems hardcoded to... whatever the JVM you're using thinks is suitable.  
> **username_4** (2023-08-10): @MatthieuM. indeed it is not, just pointing out the same "constructible hashcode" thing  
---
### Answer by username_11 on 2023-08-09. Score: 3
Don't enforce, expose to derive it
As you noted, it is infeasible to impossible for a compiler to formally verify general user code. The difficulty arises because the implementation of these standard traits are encapsulated away in implementation methods. It is hard to verify general code, but it is not necessary to verify these cases if you generate them.
Equals
== or .equals() methods are generally implemented by inspecting internal properties for equality, short circuiting on the first fail. Code like this:
def equals(Object other) as bool
{
    if ( other is Type.Of( this ) )
    {
        if ( propOne != other.propOne ) return false;
        if ( propTwo != other.propTwo ) return false;
        return true;
    }
    return false;
}

This is tedious to write, but it is very easy to do contract correct derive it, if the relevant internal properties are annotated for this.
Something like:
#[derive(Eq(propOne,propTwo)]
class X
{
    var propOne as TypeX
    var propTwo as TypeY
    var otherNotIdentifingProp as UnsafePointer
}

So the compiler can both generate and validade that each element within the == chain has a valid equals implementation.
User defined implementations of equals should be possible, but discouraged:
unsafe def [Eq] (Object other) as bool { return rand() % 3; }

Hashs
User defined hashcodes have almost the same properties as the user defined equality, with the extra requisites that it should be consistent (same hash if two objects compare equal) and be stable (do not change before invocations).
So (the only?) way to solve this is by deriving it in tandem with any user-defined == derivation.
#[derive(Eq(propOne,propTwo),Hasher]
class X
{
    //Hasher only exists paired with Eq
}

But I would argue that hashing is not a special contract in the language's semantics, but a normal contract for the language's collections library, and because of that, it should be a interface on collection namespace. Something like
interface HasherInterface
{
    private HashCode( Hasher hasher ) as u32
    {
        // Hasher as parameter to facilitate by collection hashing algorithm,
        // and because oCERT-2011-003 will haunt us forever
        // http://ocert.org/advisories/ocert-2011-003.html
    }
}

Because of its special relation with equality, any class automatically derived with Ed,Hasher should automatically implement HasherInterface too, and direct implementation of HasherInterface should be discouraged as unsafe.
Having a separate, opt-in interface for stable hashing is the first step to avoid silently bugs, and it is an extra reason for not having methods in top types, so only capable objects expose this capacity.
Ord
Ordering is easy, but separated from equality or hashing, for SortedList/SortedDict collections:
// DTO value type, all fields mutating. Eq, but not Hasher

struct Signal
{
    var date as DateTime;
    var observed as int;

    def derive Eq(observed);
    def derive Ord(date);
}

// DTO reference type, all fields mutating. Not Eq or Hasher, but Ord

class Person
{
    var id as int;             // pk, db generated (mutating)
    var firstName as string;
    var lastName as string;

    def derive Eq(id), Hasher; // compiler error
    def derive Ord(id)         // default implementation for sorted collections

    // DRY: auto generate common OrdBy$name to avoid repetitions
    // also, guarantees total order in this cases.

    def derive OrdBy("LastFirst", lastName, firstName);
    def derive OrdBy("FirstLast", firstName, lastName);

    // var list1 = new SortedList();
    // var list2 = new SortedList();

}
> **Comments:**
> **username_0** (2023-08-09): Indeed, hashing is normally only used in some collection types in the standard library. However, if it could be enforced that hashes are stable and consistent with equals, then hashes could be cached, and the `==` operator could plausibly compare hashes as a shortcut for equality of complex nested objects.  
---
