[spec] Reverse subtyping

[rossberg]

This (finally) adds the ability to do reverse subtyping on records and variants. I tried to include various motivation, explanation, and some simple examples to make those rather exotic rules clearer.

Also filled in the missing pieces of lexical syntax for values.

[chenyan-dfinity]

LGTM. Just some typo.

[nomeata]

It seems that this rule is actually just an instance of the

not (<datatype> <: <datatype'>)
---------------------------------
opt <datatype> <: opt <datatype'>

rule, isn’t it?

Ah, but they have different elaboration of course… this makes your rules overlapping (I think you avoided that before…) A problem? Since this is just defining a binary relation on types at this point (and not an elaboration) it feels strange to use more rules than necessary.

Maybe it’s worth defining <: in a non-overlapping way, with simply an unrestricted

---------------------------------
opt <datatype> <: opt <datatype'>

And then doing the different cases in the elaborated version.

Or simply only define the elaborated version…

But I thought we’d agree we need different relations for “sensible evolution” and “decoding”?

[rossberg]

Ah, but they have different elaboration of course… this makes your rules overlapping (I think you avoided that before…) A problem?

Yes, it would be better if this wasn't there. Same problem as above. For now, I added similar handwaving to pepper over the non-determinism.

But I thought we’d agree we need different relations for “sensible evolution” and “decoding”?

I realised that doesn't actually work. You need to allow all of decoding in the evolution check, because cases like that might not be under your own control: some type you use may originate from another canister, that has performed multiple evolutionary steps that are transitively non-coherent, but you have missed the intermediate step that would avoid the "ugly" transitive case when you upgrade yourself.

Hence the informal language in L785+ instead, about discouraging users to create that case and implementations to warn about it.

IOW, we need the completeness property after all, even if some cases hopefully never occur in practice if everybody follows good style.

[nomeata]

I don't follow the example. Even if you miss a step, and even if there there is incoherence, the “interface evolution” relation would still be transitive, woudn’t it? But maybe there is some complicate higher-order case where some canister is in the unfortunate situation where it is force to upgrade it’s interface in an undesirable way.

[rossberg]

Our previous conclusion was (unless I misremember something) that the transitive rule (opt t <: opt t' with incompatible t, t') should not be allowed in the upgrade check, because that check always deals with a single evolutionary step where you simply shouldn't be doing that. And that we hence should define two relations, one with and the other without this rule (or something like that).

But the assumption that the check always deals with a single evolutionary step is bogus if your interface has to adapt to (the latest version of) somebody else's interface types, whose evolution might have a different pace, and who makes bad transitive evolutionary choices outside your control. In that case you may need the "bad" rule on options even during upgrade checks.

[nomeata]

Our previous conclusion was (unless I misremember something) that the transitive rule (opt t <: opt t' with incompatible t, t') should not be allowed in the upgrade check,

yes… but

because that check always deals with a single evolutionary step where you simply shouldn't be doing that

wasn’t the reason, I think. I thought the reason was that we only had problems when you need the bad rules due to transitivity because you composed two serivces, and each was doing one (or more) sensible steps. But the transtive relation was only relevant for decoding, not an actual service evolution.

That’s why I hope we can have a “can sensibly evolve” relation (probably with polarities), that’s transitive, and a separate relation “can be decoded at” relation that has the unwanted relations.

But maybe I am too optimistic, and there will always be corner cases where a service needs to change its interface is a “bad” way.

[nomeata]

I don’t think we can allow such subtyping premises on the elaborated rules, as these define deserialization.

Shouldn’t this rule (without the premise, and with the if ∃ elaboration) subsume the normal rule?

[rossberg]

Yeah, I tried to keep the structure of the rules without elaboration. But I think the problem is that this rules try to express a phase separation that doesn't actually exist. All the rules should be considered "runtime". I removed the other rule and reformulated this one non-deterministically and added a comment admitting that the formulation is somewhat hand-wavy. Doing it properly would require a 4-place relation like v:t <: v':t', I think, but I'd prefer leaving that for another time.

[nomeata]

Yes, we can clean up separtely.

I don’t think it’d be a four-place relation: Didn’t we determine that the input data should be considered untyped (and the type description just be an encoding help)? So I’d expect v <: v' : t or maybe more suggestively v ~> v':t.

[rossberg]

I suppose we could phrase it like that, but that would be a bit of a disconnect with the actual serialisation format, which does include a type -- it just may not be "principal".

[nomeata]

But that disconnect would be intentional: Didn't we just last week realize that it was misguided to take that type as more than just a way to help understand the binary structure of the value?

I think the conceptual phase distinction between “decoding binary to abstract value” and “interpreting a value at the expected type” is very helpful (and how many implementatoins will naturally approach this, too).

[rossberg]

@nomeata, PTAL.

[rossberg]

Yeah, I tried to keep the structure of the rules without elaboration. But I think the problem is that this rules try to express a phase separation that doesn't actually exist. All the rules should be considered "runtime". I removed the other rule and reformulated this one non-deterministically and added a comment admitting that the formulation is somewhat hand-wavy. Doing it properly would require a 4-place relation like v:t <: v':t', I think, but I'd prefer leaving that for another time.

[rossberg]

Ah, but they have different elaboration of course… this makes your rules overlapping (I think you avoided that before…) A problem?

Yes, it would be better if this wasn't there. Same problem as above. For now, I added similar handwaving to pepper over the non-determinism.

But I thought we’d agree we need different relations for “sensible evolution” and “decoding”?

I realised that doesn't actually work. You need to allow all of decoding in the evolution check, because cases like that might not be under your own control: some type you use may originate from another canister, that has performed multiple evolutionary steps that are transitively non-coherent, but you have missed the intermediate step that would avoid the "ugly" transitive case when you upgrade yourself.

Hence the informal language in L785+ instead, about discouraging users to create that case and implementations to warn about it.

IOW, we need the completeness property after all, even if some cases hopefully never occur in practice if everybody follows good style.

[nomeata]

Maybe not in this PR, but reading this I get a strong urge to re-write the spec in terms of

• A relation T <:: T' of “good” updates, that is more restrictive that what we allow (in particular, if your service defines an optional field and later removes it, this is marked using opt null).
• A set V of untyped values (essentially the AST of the encoded values).
• A relation V : T to describe the values of the types (likely without built-in subtyping, i.e. {foo = true} /: record {}, as it is not needed here)
• A type-indexed decoding function T ~> (V -> T ∪ {fail}), which by construction ignores the type annotation on the input value (V is the set of Candid values), and models decoding failure explicitly (which is needed to describe the backtracking behavior).

And then we can describe (and prove!) properties that we want to hold for these things, e.g.

• ∀ t ∀ v ∈ V. t ~> f ⟹ (f v) = fail ∨ (f v) : t
• ∀ t ∀ v : t. (f v) = v (round-tripping is possible)
• <:: is transitive
• ∀ t1 t2 ∀ v ∈ V. t1 <:: t2 ⟹ t1 ~> f1 ⟹ t2 ~> f2 ⟹ (f2 v) ≠ fail ⟹(f1 v) ≠ fail
• (Something similar for the polarity switched version of <::, if it needs polarities)

But maybe not in this PR.