The power of subtyping system
I’ve been using Java, JavaScript with Flow as static type checker for a while at work and I found the idea behind really worth sharing because it is also implemented in other OOP programming languages. This article will address to everyone even those who don’t have much knowledge about JavaScript or Flow.
Before digging into complex mathematical concepts about subtyping system, let’s be clear about what it is and why it is so important.
In theory, a type represents a set of values that follow some condition. The subtyping system holds all these sets of values and represents relations that exist between them.
We refer to a type A as a subtype of a type B if the set of values represented by A is a subset of the one represented by B. B is so-called supertype of A. This is equivalent to the fact that a value of type A can be used in any context that expects a value of type B.
This conclusion is interesting for programming languages because it helps us avoid type errors: when a context that expects a value of B, actually receives a value of a type C that isn’t a subtype of B. It’s one of the main reasons a program fails at compilation or execution.
Before going further, I would like to emphasize on the fact that a type is not a class. For example, in Kotlin String is a class and a type at the same time. But String? is a type and not a class.
Let’s go through some subtyping rules for some common types such as primitives, function, object and generic types.
In most mathematical theories, we denote if a
type Ais a subtype of atype BbyA <: B. So we will use this notation when it comes to explain some concepts below. We will also walk through some examples written in JavaScript and type-checked with Flow.
Primitives
This is pretty straightforward. Following the example below, X represents the set of all numbers, Y represents 1, 2, 3 which is a subset of all numbers. So Y is a subtype of X.
Any value 1, 2 or 3 can be used in any context that expects a number value.
Function types
I think this section is one of the most confusing topics for anyone who reads about it for the first time. So let’s go through it carefully.
We denote by f: X -> Y a function f that takes an input of type X and returns an output of type Y. What will be a subtype of the type of f?
In order that a function f': X' -> Y’, can be used in place of f everywhere (i.e. type of f’ <: type of f), f’ must be able to accept any input of type X and must have all outputs of type Y, just like f.
f’can initially accept input of typeX’. Now any value of typeXcan be a possible input forf’, so the set of values thatXrepresents must be a subset of the one represented byX’. In other words,X <: X'.f’can only have outputs of typeY’. Now all these possible outputs must be of typeY, so the set of values thatY’represents must be a subset of the one represented byY. In other words,Y’ <: Y.
In short, (X' -> Y') <: (X -> Y), if X <: X' and Y’ <: Y.
Example:
This is usually referred to as contravariant input and covariant output. Contravariant because X <: X' is the opposite direction of f’ <: f, covariant because Y’ <: Y is the same direction of f’ <: f. In practice, I try to avoid these fancy words while explaining because they bring some confusion rather than help understanding the problem.
IMPORTANT: Why this contravariance input might be so confusing for developers? Because one can expect that it’s always possible to pass a value whose type is subtype of the type expected for input argument. But note that we are in subtyping rule for function types, i.e. how a function type can be substituted with another, not for the input argument itself.
Object types
Some might think that subtyping rule for object types will depend on whether the corresponding class is subsclass i.e. inherits from another. But in case of JavaScript, unlike Java, it allows us to have an object without instantiating a class.
In most common cases, an object type A is subtype of another object type B when A contains at least all attributes of B and whose types are subtypes of the ones of B. Here is an example for illustration:
B holds all objects that have a field called name with a string value. A holds all objects that have a field called name with a string value and also another field called age with a number value, which is a subset of those held by B. So we have A <: B.
A bit more complex example:
From the subtyping function rule above, it’s clear that we can consider second object is of type Person and the type checker won’t throw any error.
Generic types
Classic example about generic subtyping is about Array like so:
We got an error at the end because doSomething might mutate its input argument, adding an Tiger to it for example, which would make dogs to be no longer a list of Dog. So by default Array<Dog> is not a subtype of Array<Animal>.
Most of the time, we need to make sure that doSomething doesn’t mutate its input argument in order to pass an Array<Dog> safely into it. We can do that with $ReadOnlyArray type like following:
In short:
In some programming languages like Kotlin, we have the same idea (https://proandroiddev.com/understanding-generics-and-variance-in-kotlin-714c14564c47).
Conclusion
Whenever it comes to static typed languages, understanding how subtyping system works can be a big gain. This concept comes from mathematics and I cannot remember how many lectures we could have at university for it.
I hope these explanations above could help you understand a bit more about subtyping system and thanks for your attention.
