Go back to Testing Programs
Chapter 03: Types
What are types
At the beginning of the first chapter we talked about different kinds of
values. We mentioned numeric values (
10 + 2,
"Hello") and Boolean values (
false). We should have
said “type” instead of “kind”, because these are the most fundamental,
or primitive, types available in essentially all languages:
A type represents a set of values. Again, as we said before, the
boolean type represents the set that contains the values
false, the type
number represents the (infinite) set of numbers from
+inf and string is the set of all
possible texts, including the empty text
"". When we have a value in
hand, we say that it “has a” type or “is of” type.
Types as an analysis result
So what can we use types for? Consider this example:
This program does not explicitly say anything about types; no type
is mentioned anywhere. However, we
can query every expression for its type. If we do this on the
expression, the type will be reported as
number[100|100], i.e., the
type of numbers between
100. The range is only one element
because of course we know the specific number, so the type can be very
precise. We can also ask for the type of the whole
val; that type is
number[100|100]. Why is this? Because by default, the type of a
val is inferred to be the type of the value’s expression. The type for
time is then
number[20|20], not a big surprise.
Ctrl-Shift-Ton a program node to query the IDE for the type of that node.
Let us add some more code:
The type of
twoDistances is more interesting. Its type is
so the types are automatically computed to reflect ranges based on the arithmetic
maybeDistances it is even more interesting, because,
depending on whether
someBoolean is true or not, the resulting value is
either 100 or 200; so the type of the
number[100|200] to make sure
it can represent both outcomes.
Actually, we could be more precise: the type is either
number[200|200], because no value other than 100 or 200 is possible. However, in this particular language, a number type can have only one value range. This means that
number[100|200]is the best way of approximating that the value is either 100 or 200. The type systems of other programming languages could potentially be more precise here.
Finally, what is the type of
speed? It is reported to be
That looks strange, it is the type of all numbers between
with an infinite number of decimal points. The reason is in this language,
a division always leads to a type with infinite precision (i.e., a real number).
Before we move on, we should probably define the term
type system: it refers to the set of rules that govern type correctness of
a program. For example, the fact that any division results in an infinite-precision
number is a rule that is part of the type system of this particular language.
Similarly, the fact that numbers “adjust” their ranges according to the
operator used, is part of the type system. The type system is also
responsible for reporting errors if users do things that are not allowed
by these rules, for example, trying to add a number and a Boolean (we will
cover this in the next paragraph). The type system is also responsible for
inferring types, which means that the type of a program node is computed
from the type of one or more other program nodes automatically. For example,
the type of the
val is inferred from the type of the expression on the
right side of the
= in the
In the example so far, we have only used type inference: our program never explicitly mentioned anything about types, but the underlying analyser has computed types for us, and we can use those types to help us understand the program. Let’s move on now to explicitly mentioning types in programs.
Types as Constraints
Look at the following program:
Here, we have used the
: notation to specify a type explicitly. More
specifically, if we specify a type for a
val, we express that whatever
expression we use on the right side of the
=, its type must be compatible
with the one given explicitly. For example, we say that the
must be a number between zero and 1,000 and it must have zero decimal
digits (zero is the default, we didn’t specify it). For the
specified a positive number with two decimal digits. The resulting
is constrained to be a positive number with infinite digits (again,
every division always gives infinite decimals in the result). How is this
Well, if you tried to use a value greater than 1,000 for the distance, or a negative value for the time, you would get an error. Importantly, you would not get the error when the program runs; instead, you get the error already when you write the program. So the analyser that is part of your programming environment performs certain checks and reports them to you as early as possible.
Note that this is kinda similar to testing. In testing, we said that you specify the same thing twice, and then check one against the other. Here, too, you specify something twice: the set of allowed values (the type) as well as a particular value. If the set does not include that value, you get an error, In some sense, the programming environment tests the program for you, based on your specification of types.
Take a look at the following example from a medical system, and you can see how types have the potential to avoid errors:
Explain better. Where is the error?
In the section above I said that “its type must be compatible” when referring to the expression used to initialize a value with an explicitly given type. So, if we have
val v : T = <expr-of-type-U>
then what does it mean for
U to be compatible with
T? Obviously, if
the same as
U, then the compatibility criterion is satisfied. So, if we wrote
val v: number[5|5] = 5
val s: string = "hello"
then everything is fine. But how about this?
val v: number[0|100] = 5
The type of the
number[5|5], so is this compatible with
It is easy to see that it is if we go back to the notion of types as sets: if the
set of values represented by
U is a subset of (i.e., is contained in) the
set of values represented by
U is compatible with
T. We also say that
U is a subtype of
T. The notion of subtyping, or more generally, specialization, will become important later in this tutorial.
Wait, but …
… why do I need to specify the type for something if, as in
vals, I also
always have to give a value and that value can never change? Well, dear reader,
you have a point here. Explicitly given types are much more useful if something
can have several values as the program executes. In such a case explicitly
given types are necessary to make the program meaningful. In the next chapter we will encounter a situation where this is the case: functions.
Continue with Functions