12 Type checking
HULK is a statically-typed language with optional type annotations. So far you haven’t seen any because HULK has a powerful type inference system which we will talk about later on. However, all symbols in HULK have a static type, and all programs in HULK are statically checked during compilation.
Tye annotations can be added anywhere a symbol is defined, that is:
- in variable declarations with
let
expressions; - in function or method arguments and return type;
- in type attributes; and,
- in type arguments.
Let’s see an example of each case.
12.1 Typing variables
Variables can be explicitely type-annotated in let
expressions with the following syntax:
let x: Number = 42 in print(x);
The type checker will verify that the type inferred for the initialization expression is compatible with (formally, conforms to) the annotated type.
12.2 Typing functions and methods
All or a subset of a function’s or method’s arguments, and its return value, can be type-annotated with a similar syntax:
function tan(x: Number): Number => sin(x) / cos(x);
On the declaration side, the type checker will verify that the body of the method uses the types in a way that is consistent with their declaration. The exact meaning of this consistency is defined in the section about type semantics. The type checker will also verify that the return type of the body conforms to the annotated return type.
On the invocation side, the type checker will verify that the values passed as parameters conform to the annotated types.
Inside methods of a type T
, the implicitly defined self
symbol is always assumed as if annotated with type T
.
12.3 Typing attributes and type arguments
In type definitions, attributes and type arguments can be type-annotated as follows:
Point(x: Number, y: Number) {
type x: Number = x;
y: Number = y;
// ...
}
The type checker will verify that type arguments are used consistently inside attribute initialization expressions, and that the inferred type for each attribute initialization expression conforms to the attribute annotation.
12.4 Type conforming
The basic type relation in HULK is called conforming (<=
). A type T1
is said to conform to to another type T2
(writen as T1 <= T2
) if a variable of type T2
can hold a value of type T1
such that every possible operation that is semantically valid with T2
is guaranteed to be semantically valid with T1
.
In general, this means that the type checker will verify that the inferred type for any expression conforms to the corresponding type declared for that expression (e.g., the type of a variable, or the return type of a function).
The following rules provide an initial definition for the conforming relationship. The formal definition is given in the section about type semantics.
- Every type conforms to
Object
. - Every type conforms to itself.
- If
T1
inheritsT2
thenT1
conforms toT2
. - If
T1
conforms toT2
andT2
conforms toT3
thenT1
conforms toT3
. - The only types that conform to
Number
,String
, andBoolean
, are respectively those same types.
Types in HULK form a single hierarchy rooted at Object
. In this hierarchy the conforming relationship is equivalent to the descendant relationship. Thus, if T1
conforms to T2
that means that T1
is a descendant of T2
(or trivially the same type). Thus, we can talk of the lowest common ancestor of a set of types T1
, T2
, …, Tn
, which is the most specific type T
such that all Ti
conform to T
. When two types are in different branches of the type hierarchy, they are effectively incomparable.
NOTE: this conforming relationship is extended when we add protocols.
12.5 Testing for dynamic types
The is
operator allows to test an object to check whether its dynamic type conforms to a specific static type.
type Bird {// ...
}
type Plane {// ...
}
type Superman {// ...
}
let x = new Superman() in
print(
if (x is Bird) "It's bird!"
elif (x is Plane) "It's a plane!"
else "No, it's Superman!"
; )
In general, before the is
operator you can put any expression, not just a variable.
12.6 Downcasting
You can use the as
operator to downcast an expression to a given static type. The result is a runtime error if the expression is not a suitable dynamic type, which means you should always test if you’re unsure:
type A {// ...
}
type B inherits A {// ...
}
type C inherits A {// ...
}
let x : A = if (rand() < 0.5) new B() else new C() in
if (x is B)
let y : B = x as B in {
// you can use y with static type B
}else {
// x cannot be downcasted to B
}