Subtyping
Structural Subtyping
extend with #structural-subtyping;
Stella is a structurally typed language, meaning that type compatibility is determined by the structure of the type rather than by its name. In the language core, an expression type must match exactly the variable/parameter type for the expression to be assignable to the variable, but by enabling the #structural-subtyping extension, the type equivalence considers if the expression type is a subtype of the variable type.
Consider the following example:
language core;
extend with
#records,
#structural-subtyping;
fn f(r : {x : Nat}) -> Nat {
return r.x
}
fn main(n : Nat) -> Nat {
return f({x = n, y = n});
}
The type {x : Nat, y : Nat} is a subtype of {x : Nat}, so an expression of the former type is assignable to the latter.
Stella supports subtyping for records and variants:
language core;
extend with
#variants,
#panic,
#structural-subtyping;
fn inc(r : <| value : Nat, failure : Unit |>) -> Nat {
return match r {
<| value = n |> => succ(n)
| <| failure = _ |> => panic!
}
}
fn just(n : Nat) -> <| value : Nat |> {
return <| value = n |>
}
fn main(n : Nat) -> Top {
return inc(just(n));
}
A record type is considered a subtype of another record type if the former defines more labels than the latter, while a variant is a subtype of another variant if it has less variants.
Top Type
extend with #top-type;
The top type (sometimes called universal supertype) is a type of which all other types are subtypes. It can be compared to the Object type in Java, for example. Values of any other type are assignable to the top type.
In Stella, it is denoted as Top.
The Top type does not convey any useful information about the content of the variable:
language core;
extend with
#top-type,
#structural-subtyping;
fn zero(r : Top) -> Nat {
return 0
}
fn main(n : Nat) -> Nat {
return zero(n)
}
To use a value of type Top, downcasting is necessary (more on that below):
language core;
extend with
#top-type,
#type-cast,
#structural-subtyping;
fn inc(r : Top) -> Nat {
return succ(r cast as Nat)
}
fn main(n : Nat) -> Nat {
return inc(n);
}
Bottom Type
extend with #bottom-type;
The bottom type, in contrast to the top type, is a subtype of all other types. A value of the bottom type is assignable to any other type.
To further illustrate the subtyping hierarchy, consider the following diagram from the Dart language documentation, in which the top type is Object?, and the bottom type is Never (the arrow represents the subtype relation):
In Stella, it is denoted as Bot.
For example:
language core;
extend with
#bottom-type,
#panic,
#structural-subtyping;
fn f(r : Nat) -> Bot {
return panic!
}
fn main(n : Nat) -> Nat {
return f(n);
}
The only expressions of type Bot are throw() and panic!. A function with a Bot return type is guaranteed to never complete execution successfully.