Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Opt subtyping: Restrict going via constituent rule #137

Merged
merged 1 commit into from
Nov 17, 2020
Merged

Opt subtyping: Restrict going via constituent rule #137

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 17 additions & 8 deletions spec/Candid.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -751,32 +751,40 @@ Additional rules apply to `empty` and `reserved`, which makes these a bottom res
empty <: <datatype>
```

#### 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.
```
<datatype> <: <datatype'>
---------------------------------
opt <datatype> <: opt <datatype'>
vec <datatype> <: vec <datatype'>
```

#### Options

An option type can be specialised via its constituent type.
```
<datatype> <: <datatype'>
---------------------------------
vec <datatype> <: vec <datatype'>
opt <datatype> <: opt <datatype'>
```
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 <datatype>
```

not (null <: <datatype>)
It can also be specialised to its constituent type, unless that type is itself optional:

```
not (null <: <datatype'>)
<datatype> <: <datatype'>
-----------------------------
<datatype> <: opt <datatype'>
```
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 (<datatype> <: opt <datatype'>)
Expand Down Expand Up @@ -959,6 +967,7 @@ Coercing a non-null, non-optional and non-reserved value at an option type treat
<v> ≠ null
<v> ≠ (null : reserved)
<v> ≠ opt _
not (null <: <t>)
opt <v> ~> <v'> : opt <t>
-------------------------
<v> ~> <v'> : opt <t>
Expand Down