Subtyping is about substitutability. That is, if we need to supply a certain type, what other types can we substitute instead? Reference capabilities are one important component. We can start by going through a few simpler cases, and then we will talk about the full chart.
First, let’s focus on the four capabilities
tag. These have a very useful property: they alias to themselves (and unalias to themselves, as well). This will make the subtyping a lot simpler to work with. Afterwards we can talk about
trn, whose subtyping is more intricate.
To keep things brief, let’s add a small shorthand. We will use the
<: symbol to mean “is a subtype of”, or you can read it as “can be used as”.
ref <: box. A
refcan be written to and read from, while
boxonly needs the ability to read.
val <: box. A
valcan be read from and is globally immutable, while
boxonly requires the ability to read.
box <: tag. A
boxcan be read from, while a
tagdoesn’t have any permissions at all. In fact, anything can be used as
That’s all there is to those four. A
ref could have other mutable aliases, so it can’t become
val, which requires global uniqueness. Likewise,
val can’t become
ref since it can’t be used to write (and there could be other
val aliases requiring immutability).
Also keep in mind, subtyping is transitive. That means that since
val <: box and
box <: tag, we also get
val <: tag. The basic cases will be explained below, and transitivity can be used to derive all other subtyping relationships for capabilities.
Subtypes of unique capabilities¶
When it comes to talking about unique capabilities, the situation is a bit more complex. With variables, we only had the six basic capabilities, but we’re talking about expressions here. We will have to work with aliased and unaliased forms of the capabilities.
From here, let’s talk about ephemeral capabilities. Remember that the way to get an ephemeral capability is by unaliasing, that is, moving a value out of a
named location with
consume or destructive read.
Subtyping here is surprisingly simple:
iso^ is a sub-capability of absolutely everything, and
trn^ is a sub-capability of
val. Let’s go through the interesting cases again with these two:
iso^ <: trn^. An
iso^guarantees there’s no readable or writable aliases, whereas
trn^just needs no writable aliases.
trn^ <: ref. A
trn^reference can be used to read and write, which is enough for
trn^ <: val. A
trn^reference has no writable aliases. A
valrequires global immutability, so we can forget our writable access in order to get
val, since we know no other aliases can write.
Temporary unique access¶
We talked about aliasing and consuming, but what about when we just use a variable without making a new alias?
iso, what type do we give to the expression
x? It would be pretty useless if we could only use our
iso variables as
tag. We couldn’t modify fields or call any methods.
What we get is the bare
iso capability. Like
ref, this allows us to read and write, but we will have to keep the destination isolated. We will get into what kind of things we can do with it later, but for now, we will talk about subtyping.
iso. As mentioned earlier,
iso^can become anything. This isn’t enormously useful, all told, but an
iso^expression with no other names is stronger than a expression pointing to an existing
trn. Similarly, we may use an expression that has no writable aliases, as an expression which has one unique writeable alias.
tag. We can’t coerce
isoto anything else since the original name is still around, but we can always drop down to
tag(which is just
box. This is quite similar, we can forget our ability to write and just get a new
boxalias to store.