Inconsistency with eq_T and ord_T signatures

[nickbattle]

When you define an "eq" or "ord" clause for a type, it creates eq_T, ord_T, max_T and min_T functions. The LRM says that these functions have the signature "T * T +> bool" or "T * T +> T", which is as you might expect. But actually both VDMJ and Overture create functions of this form:

types
	R ::
		a : nat
		b : nat
	eq r1 = r2 == r1 = r2
	ord r1 < r2 == r1.a < r2.a;
	
	T = nat
	eq t1 = t2 == t1 = t2
	ord t1 < t2 == t1 < t2;

> env
ord_R = (R * R +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (nat * nat +> bool)     <--- NOTE
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (nat * nat +> bool)      <--- NOTE
eq_R = (R * R +> bool)
> 

Note that all of the functions use the type as a parameter apart from eq/ord of the named type T. The reason for this is that the eq and ord clauses shown simply compare their arguments, and if they were of type T that would recurse (stack overflow). So they are created using the RHS of the named type, "nat" in this case.

So firstly we have an inconsistency, since eq_R is defined in terms of Rs, and that stack overflows in the example above(!). You cannot directly compare records, so the ord_R function is OK, but again it is inconsistent with ord_T's signature. The min_/max_ functions are fine, as they are created internally rather than using a user clause.

Lastly, the LRM says that the signatures of these functions are all R * R +> ... or T * T +> ....

We need to be consistent, decide how to solve the "eq a = b == a = b" and "ord a < b == a < b" cases, and then maybe update the LRM (and possibly the tools!)

[tomooda]

The syntax is defined as

type definition = identifier, ‘=’, type, [ invariant ], [ eq clause ], [ ord clause ]
                  | identifier, ‘::’, field list, [ invariant ], [ eq clause ], [ ord clause ] ;

and I think ord_T must be typed as T * T +> bool because the ord clause is on the LHS of the type synonym.

For the infinite recursion, I think one good way is to pre-define eq_ that does the primitive equality comparision and use it in the body of the eq clause, just like the super call in Java.
I'd also add you can process all those overloading resolutions before the execution by applying macro expansions (each instantiation of generic functions needs the macro expansions, too, in this case!).

[nickbattle]

At the moment, T = nat ord a < b == a < b would get turned into an explicit function definition like this:

ord_T: T * T +> bool
ord_T(a, b) == a < b;   <-- This recurses

I suppose we could include an implicit "let" before the body expression to re-define the types:

ord_T: T * T +> bool
ord_T(a', b') ==
    let a:nat = a', b:nat = b' in
        a < b;   <-- This is now ok

It's a bit more difficult with records because the rhs type would have to be composed:

eq_R: R * R +> bool
eq_R(a', b') ==
    let a:compose R' of x:nat y:nat end = a', b:compose R' of x:nat y:nat end = b' in
        a = b;   <-- This is now ok

[paulch42]

On a related point, the LRM (section 3.5) states the order relation must be a strict partial order. In that case, the type of the order relation must be T * T -> bool, not T * T +> bool. Similarly, the min and max functions can't be total.

This would then raise the question, should the equality function be total or partial. Again it is stated in the LRM (section 3.4) the defined equality must be total. However, note the default equality relation for a basic or compound type (sections 3.1 and 3.2) is always specified with the partial function type.

[nickbattle]

Incidentally, if we add an invariant clause to the types, we get these extra signatures:

inv_T(nat) = (nat +> bool)
inv_R(R) = (R +> bool)

Note that the one for T has arguments that match the RHS not T. But R is not the same(!), which has been a long standing problem. You can't test an R value using inv_R because in order to create the argument you have to have met the invariant anyway.

[tomooda]

not a solution but just an idea memo.
how about

types
	R ::
		a : nat
		b : nat
	inv mk_R(a, b) == something;

deriving inv_R(R) = (nat*nat +> bool)
I know this is infeasible because this would break backward compatibility.

[nickbattle]

We did consider something like that years ago when we first came across the problem. It doesn't really break compatibility in the sense that no one could really be using record invariants anyway!

[tomooda]

another idea is a postfix that tears down the inv, eq, ord clauses. I.e.

types
	R ::
		a : nat
		b : nat
	inv mk_R(a, b) == something;

is equivalent to

types
	R! ::
		a : nat
		b : nat;
	R = R! inv mk_R(a, b) == something;

deriving inv_R(R) = (R! +> bool)
where ! is a postfix to tear down the inv, eq and ord clauses.

[pglvdm]

My recommendation would be that we everywhere would use the name of the type (also with records) for all these extra functions BUT with a semantics which states it does not recurse for all these generated functions (inv_T, eq_T and ord_T).

[nickbattle]

"With a semantics which states it does not recurse" sounds like a special evaluation mode that applies to (what?) specific typed expressions within a function body (perhaps carried into functions that it calls?), so that a = b or a < b has different semantics in different places. That sounds like trouble, since the same typed expression has different meanings depending on (what?) the call stack.

I think we have two distinct cases. First, the eq/ord case, where you could require the user to say let x':nat = x, y':nat = y in ... if they want to refer to RHS values, like eq a = b == a = b, though it isn't as easy with records. Second, the inv_T argument case, which is about how to apply the function, not so much what it does.

If we say that inv_T parameters are special and don't have the invariant applied, you still can never call the function explicitly except for legal values, since you have to create a T value to pass, which isn't in a special context. So I'm not sure how this helps? You could pass a nat value and say that wasn't converted to T, but that's effectively the same as saying it's inv_T: nat +> bool. And again it isn't as easy with record invariants.

Can you give some examples of how your idea would work?

[pglvdm]

If we take the original examples:
types
R ::
a : nat
b : nat
eq r1 = r2 == r1 = r2
ord r1 < r2 == r1.a < r2.a;

T = nat
eq t1 = t2 == t1 = t2
ord t1 < t2 == t1 < t2;

env
ord_R = (R * R +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (nat * nat +> bool) <--- NOTE
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (nat * nat +> bool) <--- NOTE
eq_R = (R * R +> bool)

I suggest to change
ord_T = (nat * nat +> bool) <--- NOTE
to
ord_T = (T * T +> bool)
and
eq_T = (nat * nat +> bool) <--- NOTE
to
eq_T = (T * T +> bool)
and then with the understanding for all implicitly generated functions the types of the generated functions are NOT checked... So e.g. for inv_R(a_r_record) does not check the argument type including its invariant (which would yield an infinite recursion).

[nickbattle]

To try to make progress with this, I've tried to implement a blend of Tomo's R! idea, together with Leo's observation at the LB meeting that other formalisms do this with "maximal" types and Peter's suggestion, which is similar. The development is in a branch called "maximal", so we can try it before committing(!).

So now, the implicit functions that require "maximal type" behaviour have T! parameter types. These are the same as T but do not include any invariant, equality or ordering clauses. The functions that don't care about this still have T parameters. If I add an invariant to each of the types in the original example, the signatures are now:

> env
ord_R = (R! * R! +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (T! * T! +> bool)
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (T! * T! +> bool)
inv_T = (T! +> bool)
eq_R = (R! * R! +> bool)
inv_R = (R! +> bool)
>

In real use (ie. explicit calls to these) we are unlikely to pass R! values (how would you create one?), but to enable this I've extended the mk_R syntax to allow mk_R!, which creates an R! value. We may not need this though.

So now things behave as you would want, I think. You can call inv_T(123) even if T values are limited to <10 etc. You can also write equality and ordering clauses that refer to the same variables (without the eq/ord), like eq a = b == a = b and that won't blow the stack. The min/max functions behave as before.

I'm still testing some of the POG (subtyping is more complex), but it's looking reasonable too.

[nickbattle]

One problem here is that the eq_T and ord_T functions, with their T! parameters, will allow you to compare values that are not actually values of the type T. That makes sense for inv_T, because you deliberately want to be able to test non-T values. But for equality and ordering, I think it only makes sense to compare genuine T values. But we still want to suppress the eq/ord within the bodies of these functions, so that we avoid recursive problems. For example:

types
	T = nat
	inv t == t < 10
	ord a < b == a < b;

> p ord_T(1,2)
= true
Executed in 0.066 secs. 
> p ord_T(2,1)
= false
Executed in 0.004 secs. 
> p ord_T(100,200)       -- This ought to be an error?
= true
Executed in 0.002 secs. 
> p ord_T(200,100)      -- This ought to be an error?
= false
Executed in 0.003 secs. 
> 

So perhaps eq/ord functions ought to include pre inv_T(a) and inv_T(b) - that is, although the parameters are T! and so have no eq/ord behaviour, they are also valid T values.

[tomooda]

How about ord_T is typed T * T +> bool and therefore a and b are typed as T, but the interpreter upcasts a and b to T! in the right-hand side of the ord clause.

[nickbattle]

Yes, that might work Tomo. It's proving quite hard to generate the correct T! values to pass to inv_T in a precondition, given the parameter patterns for the ord clause can include ignore patterns. With an upcast, that would be easier, though it would need to be a special case in the type checker too, I think, which is a bit ugly.

I'll try it later :-)