Design proposal: Type canister upgrades via an "Evolves to" relation, _not_ with subtyping.

[matthewhammer]

This week in Zurich, the ActorScript team discussed the type discipline for canister upgrades.

We had been thinking (collectively) that we want subtyping to play a role here. I've never accepted that, and now I'm certain it's wrong. @ggreif gave me some useful hints during that discussion that have since germinated into a fuller idea than I had understood at the time. I've tried to capture it here.

Also, before leaving, @crusso has humored me with lots of helpful discussion today. Those discussions are (mostly) reflected here too, though the full set of on-paper rules are currently missing here.

I'm writing up the current status of that discussion here to memorialize it and to continue it more broadly, with @rossberg @nomeata @chenyan-dfinity @kritzcreek

[nomeata]

Didn't think about it in detail yet, but it's indeed a good approach to question whether the function arrow needs to be contravariant. All our impossibility results in Zurich depend on that assumption, and seeing if we can get rid of it is worthwhile. (How we call the resulting relation is less important :-))

[nomeata]

Ok, taking a second look now. Lot’s of prose … but I feel I can summarize the content (in a slightly unflattering way, I guess) as: “Let’s explore a relation that elaborates into conversion functions both ways and where all type constructors are covariant”.

But I miss the rules for this relation, and also for the relation on values that you propose! (Or at least some rules for simple cases, to check soundness).

BTW: The two relations form not just a galois connection, but a galois embedding, because one of the compositions is the identity, it is a galois embedding, if I remember correctly.

[rossberg]

It's worth exploring whether we can decouple evolution from the subtyping relation. However, I don't understand how that would magically make functions co-variant. Functions very much invert the direction of time or the evolves-to relation for their arguments (i.e., a potentially older client passes arguments to a new server, which then returns new results to the older client), and this switches again in the higher-order case (an old client passes an old function to a new server, which invokes it with new arguments consumed by the old function, which then returns old results to the new server).

I'd need to see the elaboration rules, i.e., how the two coercions e1 and e2 are used, especially in the higher-order case. Somehow their use has to switch direction for function arguments. I believe it if I see rules that are type-correct and where e2 does not end up being equivalent to the usual contra-variant coercion. ;)

[nomeata]

Ok, let’s try to come up with some simple upgradeable types. It seems because of the two functions needed, we would not have nat $> int. That’s fine with me, it’s cute, but I can live with that.

So maybe a small example to exercise it through is extending a variant type, and the simplest form is null $> opt t. For arguments that makes perfect sense, and in the other direction we can map everything to null:

null $> opt t ~~> (λnull. null; λ_. null)

Now assume the following method after upgrade from type null -> null:

func foo(a : opt nat) : opt nat = { switch a { case null ?42; case x ?(x+1) }

I can see what happens when the argument is passed as null : null – the first function is applied, turning this into null : opt nat, and we can apply the function. But what do you expect this function to return? ?42 : opt nat and the receiver of the reply (i.e. the caller of foo) somehow converts the value? Or does the caller of foo somehow indicate at which type it called foo and then foo turns ?42 : opt nat into null : null?

The question of “where” things are happening is maybe not so important, but if the answer is “the receiver of the reply”, then we definitely need some form of coherence result, i.e.g

   to $> tn ~~> (u1, d1) // to for type old, tn for type new, u for upgrade, d for downgrade
 ∧ to $> tn ~~> (u2, d2)
⟹ d2 = d1

because that code cannot know how the other party upgraded.

If the answer is “the upgrading party applies these functions”, then we may get away without coherence, but (I think) only if the you record the evolution of the canister. Which has similar implications than Dom’s upgrade plan, where you need tooling to know old versions of your code.

So I assume we want a coherent setup for now.

The next question is: Does this work in the higher order case (which, I believe, is where non-contravariant function arrow rules frequently break down)? And to answer this, I think we need more clarity as to “when do I apply u and when do I apply d”. I wonder if this ends up being a different phrasing of the ideas we had somewhere else where we would track, in the subtyping judgment, whether we are in an “incoming position” or “replying position”, and apply different subtyping rules (here: applying u or d). I don't remember where Andreas wrote down the rules for that, and by which reasoning he discarded it.

[rossberg]

I don't remember where Andreas wrote down the rules for that, and by which reasoning he discarded it.

Can't find the discussion right now either, but it got dropped because it also wasn't correct in the higher-order case, exactly because it tried to not switch directions contra-variantly.

FWIW, I'm tending towards going back to the rules that allow {a : opt T} < {} < {a : opt T}. I think the coherence issue is avoided if there is no separate transitivity rule (i.e., transitivity is admissible). That would still mean that, technically, the semantics of composing the coercions for multiple upgrades may not be coherent -- i.e., a new parameter version could accidentally pick up a very old field. But I wonder whether that matters in practice. In practice, we would recommend to not contra-variantly remove optional fields. Instead, deprecate them by turning them into opt top (which we could shorthand deprecated). And this is only an issue anyway for records that only occur contravariantly, since any covariant appearance would immediately rule out such a removal.

[nomeata]

So we’d still be able to prove

t1 <: t2 ∧ t2 <: t3 ⟹ t1 <: t3

but not

t1 <: t2 ~> f1 ∧ t2 <: t3 ~> f2 ⟹ t1 <: t3 ~> f2 ∘ f1

Maybe that works, but it surely doesn’t improve my sleep ;-)

[rossberg]

@nomeata, yes exactly. My sleep is fucked up anyway. :)

[nomeata]

for multiple upgrades

The problem is less pressing for multiple upgrades of the same, sag, argument, but rather for independent upgrades, where one side changes the return type and the other side an argument side. But maybe not even that is too pressing…

But if you have {a : opt T} < {} < {a : opt T}, i.e. allow you to go “both ways” which depth subtyping do we use?

Does this lead towards a world where we end up with an equivalence relation describing mutually compatible types, rather a partial order?

[rossberg]

for independet upgrades, where one side changes the return type and the other side an argument side.

Hm, not sure how that scenario can arise on the platform. Normally every canister has a clear owner, who also is the only one that can initiate an upgrade and change the type of a function in its interface. Perhaps in some higher-order case, but I can't think of anything concrete.

But if you have {a : opt T} < {} < {a : opt T}, i.e. allow you to go “both ways” which depth subtyping do we use?

Sorry, you lost me there. Operationally, you can only ever go one (direct) way, which is determined by the two types involved. The compiler itself never composes coercions.

[nomeata]

Perhaps in some higher-order case, but I can't think of anything concrete.

Yes, higher order (everything would be simple in the single order case…)

Canister A has foo : (({} -> ()) -> ()), canister B has bar : {} -> (), canister C invokes A.foo(B.bar), and now A evolves to foo : (({opt int} -> ()) -> ()) (using the “can add any field when going down the hierarchy” rule) and B evolves to foo : (({opt int} -> ()) -> ()) (using the hard-fought for “can add optional fields to arguments” rule), and C is untouched. But maybe such confusions are simply unavoidable in a structurally typed world.

Sorry, you lost me there

You just explained how to go from

type T = {}
shared foo : T -> T

to

type T = {opt nat}
shared foo : T -> T

because you allow both removing and addition opt fields. But we still have to go down the partial order in result types and up in argument types. So we cannot evolve the interface deeply using normal subtyping, i.e. can’t go to:

type T = {opt int}
shared foo : T -> T

[rossberg]

Ah, I see. No, you can't use depth subtyping that way, but that can never possibly work AFAICS. But importantly, you can use record extension deeply, e.g.:

// Version 1
type T = {Text}
type U = {T; T}
foo : U -> U
bar : (U -> U) -> ()

// Version 2
type T = {Text; opt Nat}
... rest unchanged

[nomeata]

that can never possibly work AFAICS

I think Matthew wants to prove you wrong in #753 :-)

This might work. Is it fair to rephrase your proposal as “when a field has an opt type, try to decode the argument opportunistically, and use whatever value you find, if you can”?

[nomeata]

Can we close this to get it off the list of open PRs?

[matthewhammer]

Can we close this to get it off the list of open PRs?

Has the conversation resolved?

I didn't allocate any time to this, and somehow missed the comments from last month in my github notification email blasts. I apologize.

I think the possible next steps to take are:

1. Close this and forget about it for some reason identified above (not sure; need to read all of the conversation still).
2. I can try to write out the rules that are on paper; I described them a little to Claudio, but haven't thought about them in a month, since Zurich, really.

[nomeata]

Well, #832 isn’t through just yet, so I guess the conversation isn’t completely resolved.

[matthewhammer]

@nomeata is trying to distill the idea down to something about optional fields; that all sounds plausible, but I can't recall the main ideas right now, since I haven't thought about them recently. They are out of cache.

I did notice that @ggreif hasn't said anything above (though he's edited some comments), or I missed it.

A lot of this idea germinated from something that he said to me when we were all in the Radiohead conference room one day in October. I'll try to remember it in fuller detail by referring to my notes today.

[matthewhammer]

This conversation can permanently move to #832

The conversation there is more relevant than these notes, which we can remove now.