Candid subtyping meta-issue

[nomeata]

We have had many attempts at solving the problem of “how to extend records in arguments of Candid functions”, but don’t have an overview (so every new attempts involes some serious github archeology). This issue tries to collect all the different variants we discussed, ideally with links such discussions (obviously tricky when discussion happend in Radiohead). I took the liberty of trying to put a little taxinomy on this.

• New types
  These variants introduce new types or variants of types. These proposals don't change the basic machinery of subtyping (there is still just one relation), so these proposals all ended being sound but not permissive enough to tick all boxes.
  • The upgraded t type constructor, with any <: upgraded null. (upgraded type constructor for IDL? #364, May 2019)
  • Adding record in { … }, with all absent fields considerd to have type null, and record out {…} with all absent fields having type any (the latter is the “normal” case) (Elaboration and some other tweaks #438, first commit, May 2019; also discussed in upgraded type constructor for IDL? #364)
  • Adding a marker on field names (e.g. record { new? : text }), so that records have some some fields with default type null and some fields with default type any (also discussed in upgraded type constructor for IDL? #364)
• Static re-interpretation of record types
  In these variants, the user still writes record { … }, but effectively this means one of the above based on where the type occurs.
  • record {…} is record in or record out, depending on position of the next enclosing function arrow (Candid record extension: The asymmetric solution #1509, May 2020, “assymmetric solutionc”)
• Multiple subtyping relations.
  These proposals introduce multiple subtyping relations (e.g. <:+ and <:-). Expressive enough, but tend to have soundness issues.
  • Polarity (version 2019), with width subtyping in negative positions. (Elaboration and some other tweaks #438 (comment), second commit, May 2019)
  • Polarity (version 2020), without width subtyping in negative positions. (Bring back polarities #1520, May 2020)
• More dynamic solutions
  Soundness enforced by a dynamic check, very expressive, downside: Very high implementation complexity on all decoders.
  • Subtyping allows any type, value is used if sent (dynamically) at subtype of the expected type (Fix IDL subtyping #832, Nov 2019)
  • Subtyping allows any type, value is used if sent (dynamically) at an equivalent of the expected type (Candid subtyping: Dynamic solution with type hash #1525, May 2020)
  • Subtyping allows any type, value is used if there exists (dynamically) a suitable subtype of both the actual and the expected type ([IDL] Optimistic subtyping #1959, Sep 2020)
  • Backtracking within opt based on opportunistic decoding: ([spec] Reverse subtyping candid#110, Oct 2020)
  • Subtype checks based on given and expected type at opt: (Spec: Do a subtyping check when decoding candid#168, April 2021)
  • Backtracking witin opt, with subtype check for references (Extensible variants candid#295 (comment), Nov 2021)
• Stateful solutions, where the history of services affects types and/or values
  • Subtyping relations that are not contravariant, “evolution” based: Design proposal: Type canister upgrades via an "Evolves to" relation, _not_ with subtyping. #753 (Oct 2019)
  • IDL types remember their history (History based IDL subtyping #1106, Jan 2020)
  • Actor references remember their type (IDL evolution via versioned references and (virtual) proxies #1150, Jan 2020)

Meta-theory:

• A formulation of what “sound” means: IDL theory: Formalize “IDL soundness” #1544

[nomeata]

(Ideally, discuss the taxinomy here, but discuss the merits of the corresponding proposals there, else this discussion will grow out of proportion.)

[matthewhammer]

Thanks for this summary. Very helpful.

As far as the relational comparison and analysis, I feel a cube-like picture coming on, reminiscent of the lambda cube. Hopefully things are not that complex, though.

[nomeata]

Just remembered there was also the “history based solution”, #1106; added. Oh, and also #1150.

[matthewhammer]

Moved the "evolution-based" idea from Oct to go with the Jan "stateful solutions", since I think it belongs with those other solutions, which subsume it (or at least, #1106 does).

[rossberg]

Here is what Cap'n Proto has to say about possible protocol evolution. They only consider compatibility of representation, and completely ignore the semantic ability to handle the changes.

[rossberg]

Addressed by dfinity/candid#110.