Subtyping: specialised to constituent type and “fix opt” introduce inconsistencies

[nomeata]

The “option type can be specialised to its constituent type” still worries me…

Here is one problem, maybe fixable, but maybe indication that this rule just doesn't fit well with the system.

With this rule, we certainly want

true ~> opt true : opt bool

But also

true ~> opt true : opt bool
true ~> opt opt true : opt opt bool
true ~> opt opt opt true : opt opt opt bool
…

So what does this mean for

type FixOpt = opt FixOpt

true ~> ? : FixOpt

Let’s try to apply the rules (with a logical variable ?X for the result).

    true ~> ?X : FixOpt
⇐ opt true ~> ?X : FixOpt      
⇐ opt true ~> opt ?Y : FixOpt -- ?X = opt Y
⇐ true ~> ?Y : FixOpt

and we are in a loop. The solution ?X = opt ?X is not allowed (our values are inductive, not coinductive – I hope!). And since we understand _ ~> _ : _ to be inductive, we should get

not (∃x. true ~> x : FixOpt)

But by the rule about “failed parses at type opt turn into null`”, this implies

opt true ~> null : opt FixOpt

which (because opt FixOpt = Opt) implies

opt true ~> null : FixOpt

which implies

true ~> null : FixOpt

by the “subtype to constituent type” rules.

This is a blatant contradiction! This means our _ ~> _ : _ relation is inconsistent!

How can that happen? Don’t all inductively defined relations well-defined? No, they are only well-defined when the relation appears only in strictly positive positoins in the rules. And our rule

not (<v> ~> _ : <t>)
-------------------------
opt <v> ~> null : opt <t>

breaks that. This would also be a major headache when trying to put this into a theorem prover.

The way to deal with that there (e.g. Coq) would be to define the relation as a well-founded function on the v (we can’t use t because the types themselves are coinductive). In all rules, the antecents only mention subterm of v. And it also (nicely) matches a real implementation which would traverse v.

Well, all rules but his one:

<v> ≠ null
<v> ≠ (null : reserved)
<v> ≠ opt _
opt <v> ~> <v'> : opt <t>
-------------------------
<v> ~> <v'> : opt <t>

Maybe we can patch around this issue (e.g. requiring <t> ≠ opt <t>) … but I am leaning towards just dropping it. It makes the formalism cleaner (a good sign) and it makes the implementation easier to get right and secure (they otherwise have to guard themselves against an infinite loop upon true ~> ? : FixOpt).

Do we have any compelling reason/use case for this rule?

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

[rossberg]

Interesting observation. I've been warming up to removing the rule.

Here is the use case for having it. Imagine a configuration parameter:

type config = record { x : nat; y : nat };
service : {
  setup : (config) -> ();
  ...
};

Now, in some iteration of the service's life time, the configuration record is extended with a new field z that supersedes the existing y by providing similar information but in a different or more expressive way:

type config = record { x : nat; y : nat; z : opt text };

At this point you actually want to be able to make y optional, because it doesn't make sense to set both y and z at the same time.

type config = record { x : nat; y : opt nat; z : opt text };

The rule allows that in a backwards-compatible way. It also is natural to have on an intuitive level.

But I agree that its meta-theoretical properties are somewhat hairy, as it evokes some of the typical problems of non-disjoint unions.

[nomeata]

Interesting use case, thanks! You could even do the following variant:

Initially, your published interface (“published interface v1”) is

type config = record { x : nat; y : nat };

Later you want to switch to text. The current candid rules allow you to publish the interface (“v2“) as if there was no y,

type config = record { x : nat; z : text };

and still be compatible with all clients (those using v1 and those using v2) by implementing the interface

type config = record { x : nat; y : opt nat; z : opt text };

Distinguishing between published interface and implementend interface (where the implemented interface is a subtype of all published interfaces) is a pattern that will emerge, I expect. It is just too useful to remove “old cruft” from the documented interface without breaking clients, so people will do it.

---

But back to the issue at hand… should we try to fix it?

This might work for a set of opt rules:

----------------------    -- NB: This rule is actually admissable
null ~> null : opt <t>

<v> ~> <v'> : <t>
-----------------------------
opt <v> ~> opt <v'> : opt <t>

<v> ≠ null
<v> ≠ (null : reserved)
<v> ≠ opt _
<t> ≠ opt <t>  -- ad-hoc protection against looping
<v> ~> <v'> : <t>
-------------------------
<v> ~> opt <v'> : opt <t>

not (<v> ~> opt _ : <t>)
-------------------------
<v> ~> null : opt <t>

This might fix the (rather formalistic) inconsistency of the previous formulation.

It does not fix the problem that a decoder needs to worry about FixOpt (detect it explicitly), or that now decoding coudn’t be implemneted in Coq as a recursive function (assuming a Coinductive type, which would be nice and elegant), because it can’t decide <t> ≠ opt <t>. So not a satisfying solution.

[rossberg]

<t> ≠ opt <t>  -- ad-hoc protection against looping

Hm, is that enough? Couldn't it still be <t> = opt opt <t> or any variation thereof?

[nomeata]

That's all equivalent, isn't it? All of these rules are written with type names already substituted (e.g. operating on infinite/coinductive rules).

[rossberg]

Doh, yes. I need a vacation.

Okay, I can't think of any other case, but is there a proof plausible argument that no such case exists?

[nomeata]

You mean another case of inconsistency/looping rules? No really.

Note that

<v> ≠ null
<v> ≠ (null : reserved)
<v> ≠ opt _
<t> ≠ opt <t>  -- ad-hoc protection against looping
<v> ~> <v'> : <t>
-------------------------
<v> ~> opt <v'> : opt <t>

could be rewritten as

<v> ≠ null
<v> ≠ (null : reserved)
<v> ≠ opt _
<t> ≠ opt _
n > 0
<v> ~> <v'> : <t>
-------------------------
<v> ~> optⁿ <v'> : optⁿ <t>

right?

[rossberg]

Hm, I guess.

So if we were to define some weight metric to prove termination, we could take the lexicographic order on pairs (|<v>|, |<t>|), where size of types is defined by the size of their (minimal) reachable graph representation. All other rules are inductive, so |<v>| gets smaller. In this rule it isn't, but |<t>| is brute-forced to get smaller (which isn't generally the case in other rules!). Makes sense?

Edit: Hm, actually no, my size metric for types is broken. If T = opt vec T, then it does not get smaller here.

[nomeata]

I guess we can prove termination if want to use the fact that the type, although coinductive, is regular (is that the right term), i.e. defined by a finite graph. In actual applications it will, but I hate to appeal to that in the metatheory (in my Coq formalization of Candid earier it was nice and elegant that I could just treat the types as coinductive, and didn’t have to worry about ids, and graphs, and environments).

[nomeata]

@rossberg I am kinda waiting on a judgment call by you here. Should we

• Simply remove t <: opt t, and have a simpler system (i.e. one that you can model in a proof assistat without too much hoops, and one that you write a decode for without too many footguns), or
• Stick to t <: opt t, add a rule for special-handling of the fix opt type, and deal with the specification, implementation and meta-theoretical complexities.

As you can tell from this loaded question, I am leaning towards the former.

[nomeata]

Hmm, here is something to consider. What if we do something like this:

not (null <: <datatype>)
not (null <: <datatype'>)    -- this is new
<datatype> <: <datatype'>
-----------------------------
<datatype> <: opt <datatype'>

<v> ≠ null
<v> ≠ (null : reserved)
<v> ≠ opt _
not (null <: <t>)   -- this is new
opt <v> ~> <v'> : opt <t>
-------------------------
<v> ~> <v'> : opt <t>

This way, we have “specialize to constituent type” only when the constituent type itself isn't opt-like, avoiding the problematic recursion, but still allowing for your use case in the comment earlier up.

(This is not completely worked out yet, and transitivity might require special care with null and/or reserved).

[rossberg]

Interesting suggestion. I suppose options of options are not something you would see often in an interface, so limiting their evolution might be okay. How confident can we be that this has no problems?

I wish we had spare cycles to mechanise this, and prevent further holes.

Edit: For the use cases discussed up-thread, it still seems relevant to support this case.

[nomeata]

How confident can we be that this has no problems?

I don’t see anything immediately wrong with it, and it seems it avoid some of the squishy meta-theoretical problems (e.g. requiring equality on co-inductive types). So I’d be fine with going that way for now, right?

Edit: For the use cases discussed up-thread, it still seems relevant to support this case.

Right, but the restricted form is enough, isn't it? The use-case, in prose is “I want to allow new clients that don’t send foo : t, while still being able to receive data from old clients, who send t”.

One could argue that this is only needed if t ≠ opt _, because if t = opt _, well, it’s already optional. So we have a use case for turning a non-optional argument into an optional (and the restricted rule provides exactly that), there is no immediately clear use case for doing that again.

[rossberg]

Yes, I agree that this supports the use case. Was a reply to your previous comment.

Okay, so let's go with this.