Subtyping: Transitivity of opt-to-constituent rule #146
Comments
|
Maybe this is all fine together with the other special behavior for |
starting a bit on a Candid formalization, focusing on the Opt-to-constituent rule. Stuck at #146, and worked around by adding restrictions to the compositional rule for opt.
|
With the extra |
|
What if you have (dynamic) |
|
This issue here isn't really about the dynamic aspects of |
|
Closing this; the narrow issue of this issue only applies to a variant of the formalism that we are not using right now, as the Coq profs in #147 shows (i.e. the opportunistic subtyping rule tapers over this problem.) |
This contains an initial formalization of Candid in Coq. It covers these types: `nat`, `int`, `null`, `opt t`, `empty`, `reserved` It considers two different formalisms: * `NoOpportunisticDecoding` This is without `t <: opt t'`, but with `t <: opt t`. Things go through, although the `opt t <: opt t'` rule has to be tweaked to keep subtyping transitive (see #146). * `OpportunisticDecoding` This is with `t <: opt t'`. Because of the negative hypotheses in the coercion relation, this can’t be defined as a simple inductive relation (which is a seroius smell!). So instead I define it as a function (which is mostly straight forward), and prove the properties there. We _could_ take this as indication that maybe our spec should also just define it via equations. We don’t gain anything from the relational presentation, I think, and implementors all anyways implement functions. Nevertheless, I did prove that the relation defined by admits the intro and induction rules that _would_ come out of the inductive relation (ignoring the negative hypotheses). This revealed some issues with the way the rules are presented, will create a PR for that soon. In both cases, I prove * Correctness of decoding * Roundtripping * Uniqueness of decoding * Soundness of subtyping * Transitivity of subtyping I do _not_ prove Higher-order soundness, because we know it does not hold (see #141). This also uses some proof-of-concept “named Coq cases“ feature, see https://www.joachim-breitner.de/blog/777-Named_goals_in_Coq.
Uh oh!
There was an error while loading. Please reload this page.
I started to do some baby steps in formalizing a “mini candid” in Coq, starting with the rules that seem safe.
But adding the “specialize to constituent type” rule is causing problems:
If the rule is
as it is now, then this is not transitive. We have
int <: opt int(by this rule),opt int <: opt opt int(by the normal rule), but notint <: opt opt int(because of thenot (null <: t2)restriction).This restriction was added in #135, upon my suggestion. Without that restriction, we have the problems described in #135, i.e. bad interaction with the “catch decoding rule”, and the problem that
doesn't make progress if
t2 = opt t2.Or, to respond to @rossberg says in #135 (comment)
I am no longer confident that this has no problems.
One way to maybe! taper over the problem is to restrict the other rule as well:
so that you can’t go from
opt inttoopt opt int… but that essentially disallows evolution underopt optand might be better served by disallowingopt opt… probably not nice. Or maybe this rule:which rules out
opt int <: opt opt intwithout ruling outopt nat <: opt intnoropt opt nat <: opt opt int?The text was updated successfully, but these errors were encountered: