Refinement Types
A Refinement Type is a subtype of some type, whose inhabitants can be described by a predicate.
It looks like this: Even = { n ∈ ℤ | n mod 2 = 0 }.
Such a type is exactly what it looks like it is: it is the type of all even integrals, meaning it is a subtype of integers.
Is the user entering some positive integer capped at some constant in the online form?
Answer: { n ∈ ℕ⁺ | n ⩽ MAX }.
As subtyping is merely a substitution rule, for all expected integrals, such a type can be substituted with all expectations met.
Singleton Types
Sometimes you want to restrict some variable to a single possible value.
That's a Singleton Type.
Some reasons of why you would do that include:
- API designer decided to return some T on success, and
false on failure. Now the type is T | false, where false is a subtype of bool.
This is common in feature-poor ecosystems like early PHP and JS libraries.
- Language says references cannot be
null; instead there is a distinct primitive null type which you must use in a union (often with some T? syntax sugar to mean T | typeof(null)). Not a subtype of anything but is starting to get common in languages with simple typesystems.
- Field-based discrimination of united records, where you have a union of two records differing by a field.
Eg. this TypeScript code: { tag: "Ok", payload: String } | { tag: "Err", errCode: Int }.
In fact, singleton string types are a really common feature, used by languages such as Erlang, Elixir, Ruby, and many Lisps, usually under names such as "tags," "symbols," or "atoms."
At all times, such a singleton type, or a union thereof as seen above, can be passed to a function expecting the supertype.
Dependent Types
Sometimes I know the specific values that will inhabit a type.
Sometimes I don't.
All I know is that it is a subtype of something.
Here are Dependent Refinement Types subtyping integrals again, sans constants:
Index (xs: List a) = { i ∈ ℕ₀ | i < length xs }
InclusiveRange (xs: List a) = (Index xs, Index xs)
Here, xs is just some variable. And both times, those types meet all expectations of their respective supertypes.
Storage-Based Types
In many, many, languages, some types are defined by their storage.
In C, exists a relation sizeof(signed char) ⩽ sizeof(short int) ⩽ sizeof(int) ⩽ sizeof(long int), and from it is derived the subtyping signed char <: short int <: int <: long int.
In other languages with well-specified bit-storage, it is even more obvious: u8 <: u16 <: u32 <: u64 <: u128 etc...
Relative Pointer Types
Remember that TypeScript union?
Well sometimes, you're writing in C, where you don't have the luxury of "union of record with comparable fields types," and all you have is a pointer that points to some place of interest.
Take this fairly common idiom:
enum tag { USR, SYS };
struct msg_t
///`msg_t*` should point only to instances of `usr_msg_t`/`sys_msg_t`'s `base` field.
{
enum tag tag;
uint64_t timestamp;
};
struct usr_msg_t
{
struct msg_t base;
string_t name;
void* args;
};
struct sys_msg_t
{
struct msg_t base;
enum sys_msg_kind_t whatever;
};
const struct msg_t* new_usr_msg(string_t name, void* args)
{
struct usr_msg_t* msg = malloc_chk(sizeof(struct usr_msg_t));
*msg = (struct usr_msg_t){
.base = { .tag = USR, .timestamp = time() },
.name = name,
.args = args
};
return &msg->base;
}
const struct msg_t* new_sys_msg(sys_msg_kind_t msgk)
{
struct sys_msg_t* msg = malloc_chk(sizeof(sys_msg_t));
*msg = (struct sys_msg_t){
.base = { .tag = SYS, .timestamp = time() },
.whatever = msgk
};
return &msg->base;
}
#define get_parent_of_ptr(ptr, m, t) (t*)(ptr - offsetof(t, m))
void disp_msg(const struct msg_t* msg)
{
switch(msg->tag) {
case USR:
const auto msg_ = get_parent_of_ptr(msg, base, struct usr_msg_t);
f(msg_->name, msg_->args);
break;
case SYS:
const auto msg_ = get_parent_of_ptr(msg, base, struct sys_msg_t);
g(msg_->whatever);
//...
}
}
In disp_msg's signature, what is msg's type?
C says it is const struct msg_t*, but we can do better.
In this struct subtyping idiom, the pointer we receive points to some tag (and associated data) that is shared across multiple subtypes and that can be used to discriminate them.
The get_parent_of_ptr operation doing pointer arithmetic clearly demonstrates this property.
So while C does not itself understand it, you, as a programmer, are supposed to understand that usr_msg_t and sys_msg_t are subtypes of msg_t.
And as language designers, we can do better!
This parameter is not just a random pointer: it is a relative pointer! Precisely, its type is (usr_msg_t § base)* | (sys_msg_t § base)*, which happens to be a subtype of msg_t*.
This is also a demonstration of where typing discipline clashes with programming languages.
We're talking of values of types which the language we use does not understand, forcing us to rely on manual dynamic code (including manual type checks, and in the case of a language like C, pointer arithmetic too), and on documentation in natural languages, none of which are actually checked by a compiler!
We Can Do Better
As I hope I demonstrated, typing discipline is a greater topic than just language features.
When designing interfaces, we are more often than not talking of types which the used language cannot express, so we rely on Human-oriented, ignored-by-compilers, documentation.
The API's code says the getUserRelations function returns an int, but the API's documentation contradicts this by saying it is an { n ∈ int | n < 100 } - a subtype of int.
That one illustration of subtypes as output may be harmless, but what about subtypes as input?
The API's code says the send_remote_msg function takes in a usr_msg_t*, and the API's documentation says it is (sys_msg_t § base)* | (usr_msg_t § base)*.
What happens if I pass in some other message pointer? What if I pass in NULL?
The documentation is clear in that I must not, but the code is way more liberal, and the compiler will never complain!
So indeed: subtypes of "primitive types" are in everything, everywhere, all at once.
1<:1 | 42<:uint8<:uint16<: ℕ <: ℤ, etc.. Alsofalse<:boolin some places because API reasons. $\endgroup$enum.IntEnumis subclass ofint. Similarlyenum.StrEnumis a subclass ofstr. Before it was added the recommended way was to use multiple inheritance fromenum.Enumandintorstr. $\endgroup$class Doublable(int)is subclassing, so I don't understand what makes you say that the question is about subtyping and not subclassing. $\endgroup$