Elaboration and some other tweaks

[rossberg]

Okay, this aims to address #364 and fix the transitivity issue by indexing the subtyping relation with a polarity that controls which record rules are applicable where:

• ordinary width subtyping (adding fields) is only available for records occurring in + polarity
• optional fields can only be removed (contra-variantly added) from records in - polarity

Admittedly, it is odd to have this on the side of co/contra-variance. The upshot is that extending a record type with an optional field creates both a co- and a contra-variant subtype! I'm not sure how else to achieve that.

Let me know what you think or whether I've been smoking crack.

Other changes:

• Untied subtyping T <: opt T, since we're no longer restricted to non-coercive subtyping.
• Renamed unavailable to reserved, which makes slightly more sense now.

[nomeata]

If opt opt nat can be specialized to opt nat by two different ways, and we do subtyping by coercion, then the coercion is not uniq and the difference is observable: is null coerced to null or some null. That's a problem, right?

[rossberg]

Ah, I think you're right, I was overeagerly removing the restriction we had before.

[rossberg]

Fixed.

[nomeata]

Overall promising! Will have to digest it more, and will want to run it past Coq eventually before committing to it.

[nomeata]

A bit fishy that the polarity of function arguments is not always negative. If the polarity affects which coercions the decoder of the functions decodes the record, then maybe it should always be negative, independent of the incoming polarity on the whole function type? (It wouldn't be a polarity then anymore, would it?)

[rossberg]

A bit fishy that the polarity of function arguments is not always negative.

That's a good question that I was mulling over for a while. I actually started out with the alternative you describe. But I believe that would be wrong. In the higher-order case, contra-variance needs to apply as usual. Consider:

type T = {}
actor { f : (g : T -> T) -> () }

What I want is that this is upgradable to

type T' = {a : opt nat}
actor { f : (g : T' -> T') -> () }

That is,

(1)  (g : T' -> T') -> ()  <:+  (g : T -> T) -> ()

should hold. Under the given rules that requires that

(2)  T -> T  <:-  T' -> T'

which in turn requires

(3) T <:- T'
(4) T' <:+ T

which is satisfied. With your suggestion the polarity of (3)-(4) would be switched and hence the wrong way round.

[nomeata]

You are arguing by what you wish to be true, which is useful, but not necessarily implies that it actually works soundly that way :-)

I wonder how to even phrase soundness precisely. I guess we'd need to specify the encoding/decoding functions (which would do the coercive subtyping) to do that.

The decoding would take the IDL type, the type encoded in the message and the encoded value as inputs (but not the subtyping derivation, which is the cause for the ambiguity mentioned earlier).

Would the encoding function just have one type input, or also take two for some reason? Or could encoding just be the identity (at this level of abstraction, ignoring the actual binary representation), and decoding is “just” the subtyping coercion, and we want to prove that it's the identity when they two types are the same, and that it it behaves well with transitivity (i.e. all ways going from one type to another, even with intermediate types, yield the same function).

Should write this formally, but not on the phone.

I'll be on a bike ride today, will think more about it.

[rossberg]

With the typed encoding we have now both encoding and decoding should only ever have to consider one type. Subtyping is completely decoupled. (At least conceptually, of course an implementation might want to fuse decoding and coercion. No coercion happens in the encoder, though.)

That means that the only correctness criteria for subtyping should be: (1) is it reflexive and transitive, (2) is there a corresponding (unique) coercion function? Both shouldn't be hard to prove (except maybe uniqueness).

[nomeata]

Agreed, but I think we want more from the coercion function, e.g. not just be a constant function that ignores the input (which would be unique).

If we have s <: t, then we want a coercion function c_st : s -> t (right?) with these properties:

• c_tt = id
• c_tu . c_st = c_su
• Something that it does not throw away information that should be visible at the super type? E.g., for each c_st there is a function g : t -> s (not necessarily unique) such that c_st . g = id? But that doesn't work, t is a too big... How else do we rule out bogus coercions?

[rossberg]

The function ought to be defined by induction on the type. That way, a sort of "parametricity" applies in each case, and in most of them it cannot create an out-of-thin air result. The exceptions are primitive types and variants, including opt. But those may be sufficiently constrained by your identity requirement.

But that isn't really an intensional property...

I think your composition condition follows from transitivity.

[rossberg]

Another way to express what I said is that coercions must be functorial mappings, i.e., for each type constructor T X and function f : X -> Y it must hold that c_{T Y}{T' Y} . f = map_T f . c_{T X}{T' X} (or some dual law when T is contra-variant in that parameter).

[rossberg]

I added elaboration rules that define the coercion function. Intuitively, it is "obvious" that it has the desired properties.

[nomeata]

Thanks for adding the coercions!

BTW, the way you write your rules, transitivity should follow, right? I.e. there is no implicit transitive closure here.

[nomeata]

I guess I can answer that myself: transitivity should be a derivable property.

Stared at it a bit and it seems to hold up. But I don't have a good intuition about the polarities to make sense of them yet. One (more value-oriented) interpretation might be the following: there are two sets of coercion functions. The positive ones interpret all absent fields as having type reserved and the negative ones interpret all absent fields as having type null.

The elaboration, when subtyping a function, wraps that function. But what really happens is that you upload a new version of the code, and the function itself receives a message with type information and then applies the appropriate coercion function to go from the message type to it's current argument type. Since we have two sets of coercion functions it is a bit unclear to me how the function knows which one to apply. Is that somehow hard coded into the function? Does this mean we need a flag on the function type (which would be not nice)?

If this doesn't make much sense to you feel free to ignore this comment until I distilled a concrete problematic example (if there is one).

[nomeata]

Ok, starting to believe that this is sound. And also starting to believe that this encodes the informal rule “when you call a function, you must not pass any record fields that the function promises to accept”. And hence dually: when decoding function arguments, there will be no unexpected fields.

I am not happy with the elobaration yet: when we pass along a function reference to a function living somewhere else, or even to a full actor, then we can't just wrap it in a coercion, can we? Is that a problem?

[rossberg]

I think in reality the coercion actually is the identity on functions, since we have an send operator than always has the necessary coercion built-in itself. It will simply perform wider coercions. I just wasn't sure how to represent that succinctly.

[nomeata]

I think I know why I wasn’t convinced yet, and why this might not fly.

The whole idea of using subtyping for canister upgrades is that there is one relation that decides whether we can upgrade a canister without breaking existing code, i.e. in all contexts. And we need to put the emphasis on one – with this proposal, we have two relations, <:+ and <-:, and it depends on the context which one is the right one. So which relation is used to decide if an upgrade is ok?

Let's assume it is <:+ (the “easier to understand“, in a way), and start with this example:

• Initial situation:
  • Canister a has method g : {} → bool; g(x) = true
  • Canister b has method h : ({} → bool) → bool; h(g) = g({})
  • Some further code is invoking b.h(a.g). Everything is fine.
• If upgrades need to go to a subtype according to <:+, then it is possible to
  • upgrade a to have g : {c : opt int} → bool; g(x) = isNull x.c (adding new optional fields)
  • upgrade b to have h : ({c : bool} → bool) → bool; h(g) = g({c = true}) (ignoring extra fields in negative polarity, I hope I got that right.)
  • Some further code still invokes b.h(a.g). Boom!

Your rules are sound (I think); what isn’t sound is allowing canister upgrades from t1 to t2 based on either t2 <:+ t1 (or t2 <:- t1). In both of the two cases, there will be contexts where it is the wrong polarity.

Or am I misreading the intention?

[rossberg]

Checking for upgrading always starts with <:+, you only switch in contra-variant position.

But I think your counter-example is a good one. It may actually show that there is no solution to this problem. Now what do we do?

[nomeata]

But I think your counter-example is a good one. It may actually show that there is no solution to this problem. Now what do we do?

There are many solutions, just no good one.

• For example, you could have two kind of records, those where missing fields are typed null (supports adding optional received fields) and those were missing fields are typed top (supports adding extra returned fields).
• You can make that distinction on a per-field basis, with a flag, that is essentially part of the name. (Optional fields have names ending in a question mark foo?).
• As above, but foo and foo? cannot be used in the same type (this is almost my propsoal with versioned when you restrict the version type be either 0 or 1).
• You drop one of the two features (i.e. adding optional received fields or additional returned fields).

Maybe we should do a phone call to reiterate and brainstorm?

[nomeata]

Are we still going to pursue the solution with polarities, or shall we close this PR?

[rossberg]

There is a fair amount of other stuff in this PR, so I reverted the polarities part to repurpose the PR for those.

[nomeata]

Would have preferred a separate PR (git checkout -p is great) might have been cleaner, but it’s fine.

I suggest to merge-squash, so that people going through git log do not get to see the polarities stuff.

[nomeata]

Should we define the language of values, and the value typing relation, before we can actually talk about elaboration? Or is it “obvious” what we mean.

[rossberg]

Let's say it's obvious enough for this to be useful. We can always increase precision later.

[nomeata]

I took the liberty and resolved the conflicts with master for you