diff --git a/spec/Candid.md b/spec/Candid.md index 1322159ef..0232a0341 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -751,32 +751,40 @@ Additional rules apply to `empty` and `reserved`, which makes these a bottom res empty <: ``` -#### Options and Vectors +#### Vectors -An option or vector type can be specialised via its constituent type. +A vector type can be specialised via its constituent type. ``` <: --------------------------------- -opt <: opt +vec <: vec +``` +#### Options + +An option type can be specialised via its constituent type. +``` <: --------------------------------- -vec <: vec +opt <: opt ``` -Furthermore, an option type can be specialised to either `null` or to its constituent type: + +Furthermore, an option type can be specialised to `null`: ``` ------------------------ null <: opt +``` -not (null <: ) +It can also be specialised to its constituent type, unless that type is itself optional: + +``` +not (null <: ) <: ----------------------------- <: opt ``` The premise means that the rule does not apply when the constituent type is itself `null`, an option or `reserved`. That restriction is necessary so that there is no ambiguity. For example, otherwise there would be two ways to interpret `null` when going from `opt nat` to `opt opt nat`, either as `null` or as `?null`. -Q: The negated nature of this premise isn't really compatible with parametric polymorphism. Is that a problem? We could always introduce a supertype of all non-nullable types and rephrase it with that. - Finally, in order to maintain *transitivity* of subtyping, two unusual rules allow, in fact, *any* type to be regarded as a subtype of an option. ``` not ( <: opt ) @@ -959,6 +967,7 @@ Coercing a non-null, non-optional and non-reserved value at an option type treat ≠ null ≠ (null : reserved) ≠ opt _ +not (null <: ) opt ~> : opt ------------------------- ~> : opt