[DAML-LF] specification for generic comparison.

[remyhaemmerle-da]

In this PR, we formalize the specification of the generic ordering implemented in #4808

This PR advances the state of #2256.

CHANGELOG_BEGIN
CHANGELOG_END

Pull Request Checklist

• Read and understand the contribution guidelines
• Include appropriate tests
• Set a descriptive title and thorough description
• Add a reference to the issue this PR will solve, if appropriate
• Include changelog additions in one or more commit message bodies between the CHANGELOG_BEGIN and CHANGELOG_END tags
• Normal production system change, include purpose of change in description

NOTE: CI is not automatically run on non-members pull-requests for security
reasons. The reviewer will have to comment with /AzurePipelines run to
trigger the build.

[remyhaemmerle-da]

The specification for contract id will be done in a separate PR.
I let a comment for that.

[cocreature]

You’re calling this section “Type order” and then you start by talking about numeric values. That doesn’t make sense to me.

[remyhaemmerle-da]

You are right, this is confusing.
This section is about only type ordering.
The main difference between type ordering and value ordering is that we need to specify the latter operationally to explain how it fails when encounter non comparable values. We do not need an operation specification for the former because the type checker will ensure that comparison of is always defined (the rules for typing 'to_any' and 'type_rep' ensure the type used do not contains variable, quanitifier not type synonyms).

Value ordering is define in the section Generic comparison functions.

[cocreature]

Suggested change

	on types that verifies the following rules::
	on types that satisfies the following constraints::

[cocreature]

Is this supposed to be lexicographic ordering on type constructor names? It’s not very clear to me.

[remyhaemmerle-da]

I replace by "comes lexicographically before"

[cocreature]

I don’t understand this rule. Are you trying to say that adding extra fields makes it bigger? If so, I don’t understand why f_n is at the end in both cases and what the point of f_m is.

[remyhaemmerle-da]

It is better now ?

[cocreature]

Maybe I’m missing something but which rules allows me to deduce that Int64 < Numeric 10?

[remyhaemmerle-da]

By transitivity (stated in the text) you have Int64 <ₜ τ σ for all τ and σ.

I replace the text by an explicit rule.

[ghost]

I don't see it @remyhaemmerle-da . There's no rule that lets you infer, for example, that τ₁ <ₜ τ₂ σ whenever τ₁ is not a type application.

[cocreature]

Yeah I also cannot find it in the text.

[remyhaemmerle-da]

@associahedron
TypeOrderStructTyApp allows you to infer trivially ⟨ ⟩ <ₜ τ₂ σ

@moritzkiefer-da Here is how I infer Int64 < Numeric 10

• Using TypeOrderTransitivity, TypeOrderInt64Date, and TypeOrderDateTimestamp you can infer that 'Int64' <ₜ 'Timestamp'.
• Combining with TypeOrderTransitivity, and TypeOrderTimestampText you can infer that 'Int64' <ₜ 'Text'
  ...
• Combining with TypeOrderTransitivity, and TypeOrderNatStruct you can infer that 'Int64' <ₜ ⟨ ⟩
• Combining with TypeOrderTransitivity and TypeOrderStructTyApp you can infer that 'Int64' <ₜ Numeric 10

[remyhaemmerle-da]

I do not like to define the rank explicitly (mapping types to integers)

[ghost]

I think it would make the spec match the code more closely, and be easier to understand, which are both better for maintenance, but if you are sure about this way then I'm not opposed.

[remyhaemmerle-da]

I want to be able to introduce a new type between two already existing.
This will oblige me to have different ranks between two specs.

[ghost]

That's fine. The type rank function is entirely formal, and would only exist in the spec, not be exposed in DAML/DAML-LF. Alternatively, you can define a formal enumeration of type ranks (instead of an type rank integer) and use the order from the enumeration.

Anyway, it is up to you.

[remyhaemmerle-da]

I did not include the rank.

[ghost]

This is fine for the spec, but if we were to actually implement LESS_EQ this way it becomes an O(n^2) algorithm. The actual implementation should calculate the relative order of two items (less than, equal, or greater than) in a single step, rather than needing two boolean steps to make the comparison.

[remyhaemmerle-da]

This is indeed a spec. The implementation is based on compare that return -1, 0 or +1 .
This was a bitter cumbersome to use formally (use the cases 'less than', 'equal to', or 'greater than').

[ghost]

Sounds good 👍

[ghost]

Do you anticipate this situation being possible? I.e. v0 <= v0' is fine but v0' <= v0 leads to error?

[remyhaemmerle-da]

I don't. I though it was simpler to specify explicitly this error case, than to prove this never happen. This would indeed go away with the compare function way. I will try once last time to go this way (I abandon twice already).

[ghost]

IMO it's fine if you want to keep the boolean presentation, but change this rule into a note that says that

     𝕆('LESS_EQ' @τ₁ v₀ v₀') = Ok 'True'
      𝕆('LESS_EQ' @τ₁ v₀' v₀) = Err t

cannot happen, and that if it happens, that's a bug.

[remyhaemmerle-da]

I simply drop the rule. I gave up a third time trying to specify with the compare approach.

[ghost]

Great job! I added some small remarks.