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:

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:

type Point(x: Number, y: Number) {
    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 inherits T2 then T1 conforms to T2.
  • If T1 conforms to T2 and T2 conforms to T3 then T1 conforms to T3.
  • The only types that conform to Number, String, and Boolean, 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
    }