N4JS Language Specification

4. Types

4.1. Overview

N4JS is essentially ECMAScript with the inclusion of types. In the following sections we will describe how types are defined and used in N4JS.

Besides standard JavaScript types, the following metatypes are introduced:

Classifiers, that is class or interface (see Classifiers)
Enum

Classifiers, methods and functions may be declared generic.

Types are related to each other by the subtype relation.

Definition: Subtype Relation

We use $s u b t y p e$ for the general subtype relation or type conformance.

In nominal typing, $T < : S$ means that $S$ is a (transitive) supertype of T. Generally in structural typing, this means that T conforms to $S$ . $< :$ is defined transitive reflexive by default.

We write $<$ to refer to the transitive non-reflexive relation, that is $T < S \Leftrightarrow T < : S \land T \neq S$

Whether nominal or structural typing is used depends on the declaration of the type or the reference. This is explained further in Structural Typing.

For convenience reasons, we sometimes revert the operator, that is $T < : S \Leftrightarrow S : > T$ . We write $T ≮ : S$ if T is not type conforming to $S$ . (cf. [Gosling12a(p.S4.10)])

Join and meet are defined as follows:

Definition: Join and Meet

A type $J$ is called a join (or least common supertype, ) of a pair of types $S$ and T, written $S \lor T = J$ , if

$S < : J$
$T < : J$
$\forall L : (S < : L) \land (T < : L) \to J < : L$

Similarly, we say that a type $M$ is a meet (or greatest common subtype, ) of $S$ and T, written $S \land T = M$ , if

$M < : S$
$M < : T$
$\forall L : (L < : S) \land (L < : T) \to L < : M$

Note that this declarative definition needs to be specified in detail for special cases, such as union and intersection types. Usually, the union type of two types is also the join.

Predefined Types Hierarchy summarizes all predefined types, that is primitive and built-in ECMAScript and N4JS types. Specific rules for the subtype relation are defined in the following sections. This type hierarchy shows any and undefined as the top and bottom type (cf. [Pierce02a(p.15.4)]) We define these types here explicitly:

Definition: Top and Bottom Type

We call $T o p$ the top type, if for all types T the relation $T < : T o p$ is true. We call $B o t$ the bottom type, if for all types T the relation $B o t < : T$ is true. In N4JS, $T o p = a n y$ , the bottom type $B o t = u n d e f i n e d$ .

null is almost similar to $B o t$ , except that it is not a subtype of undefined.

Figure 2. Predefined Types Hierarchy

For every primitive type there is a corresponding built-in type as defined in [ECMA11a], e.g. string and String. There is no inheritance supported for primitive types and built-in types – these types are final.

Although the diagram shows inheritance between void and undefined, this relationship is only semantic: void is a refinement of undefined from a type system viewpoint. The same applies to the relation of Object as well as the subtypes shown for string and String.

Example 6. Type Examples, Class Hierarchy

In the following examples, we assume the following classes to be given:

// C <: B <: A
class A{}
class B extends A{}
class C extends B{}

// independent types X, Y, and Z
class X{} class Y{} class Z{}

// interfaces I, I1 <: I, I2 <: I, I3
interface I
interface I1 extends I {}
interface I2 extends I {}
interface I3 {}

// class implementing the interfaces
class H1 implements I1{}
class H12 implements I1,I2{}
class H23 implements I2,I3{}

// a generic class with getter (contra-variance) and setter (co-variance)
class G<T> {
    get(). T;
    set(x: T): void;
}

4.2. Type Expressions

In contrast to ECMAScript, N4JS defines static types. Aside from simple type references, type expressions may be used to specify the type of variables.

4.2.1. Syntax

The listing EBNF Type Expression Grammar summarizes the type expression grammar. Depending on the context, not all constructs are allowed. For example, the variadic modifier is only allowed for function parameters.

References to user-declared types are expressed via ParameterizedTypeRef. This is also true for non-generic types, as the type arguments are optional. See Parameterized Types for details on that reference.

For qualified names and type reference names, see Qualified Names

The type expressions are usually added to parameter, field, or variable declarations as a suffix, separated with colon (:). The same is true for function, method, getter or setter return types. Exceptions in the cases of object literals or destructuring are explained later on.

Example 7. Type Annotation Syntax

The following two listings show the very same code and type annotations are provided on the left hand side. For simplicity, string is always used as type expression.^[10]

var x: string;
var s: string = "Hello";
function f(p: string): string {
    return p;
}
class C {
    f: string;
    s: string = "Hello";
    m(p: string): string {
        return p;
    }
    get x(): string {
        return this.f;
    }
    set x(v: string) {
        this.f = v;
    }
}

var x;
var s = "Hello";
function f(p) {
    return p;
}
class C {
    f;
    s = "Hello";
    m(p) {
        return p;
    }
    get x() {
        return this.f;
    }
    set x(v) {
        this.f = v;
    }
}

The code on the right hand side is almost all valid ECMAScript 2015, with the exception of field declarations in the class. These are moved into the constructor by the N4JS transpiler.

4.2.2. Properties

Besides the properties indirectly defined by the grammar, the following pseudo properties are used for type expressions:

Properties of TypeExpression:

$v a r$: If true, variable of that type is variadic. This is only allowed for parameters. Default value: false.
$o p t$: If true, variable of that type is optional. This is only allowed for parameters and return types. This actually means that the type T actually is a union type of Undef|T. Default value: false.
$o p t v a r$: $o p t v a r = v a r \lor o p t$ , reflect the facts that a variadic parameter is also optional (as its cardinality is $[0 . . . n]) .$
$e n t i t y$: Pseudo property referencing the variable declaration (or expression) which owns the type expression.

4.2.3. Semantics

The ECMAScript types undefined and null are also supported. These types cannot be referenced directly, however. Note that void and undefined are almost similar. Actually, the inferred type of a types element with declared type of void will be undefined. The difference between void and undefined is that an element of type void can never have another type, while an element of type undefined may be assigned a value later on and thus become a different type. void is only used for function and method return types.

Note that not any type reference is allowed in any context. Variables or formal parameters must not be declared void or union types must not be declared dynamic, for example. These constraints are explained in the following section.

The types mentioned above are described in detail in the next sections. They are hierarchically defined and the following list displays all possible types. Note that all types are actually references to types. A type variable can only be used in some cases, e.g., the variable has to be visible in the given scope.

ECMAScript Types

Predefined Type: Predefined types, such as String, Number, or Object; and .
Array Type: Array Object Type.
Function Type: Described in Functions, Function Type.
Any Type: Any Type.

N4Types

Declared Type: (Unparameterized) Reference to defined class Classes or enum Enums.
Parameterized Type: Parameterized reference to defined generic class or interface; Parameterized Types.
This Type: This Type.
Constructor and Type Type: Class type, that is the meta class of a defined class or interface, Constructor and Classifier Type.
Union Types: Union of types, Union Type.
Type Variable: Type variable, Type Variables.

Type expressions are used to explicitly declare the type of a variable, parameter and return type of a function or method, fields (and object literal properties).

4.3. Type Inference

If no type is explicitly declared, it is inferred based on the given context, as in the expected type of expressions or function parameters, for example. The type inference rules are described in the remainder of this specification.

Definition: Default Type

In N4JS mode , if no type is explicitly specified and if no type information can be inferred, any is assumed as the default type.

In JS mode, the default type is any+.

Once the type of a variable is either declared or inferred, it is not supposed to be changed.

Given the following example.

Variable type is not changeable

var x: any;
x = 42;
x-5; // error: any is not a subtype of number.

Type of x is declared as any in line 1. Although a number is assigned to x in line 2, the type of x is not changed. Thus an error is issued in line 3 because the type of x is still any.

At the moment, N4JS does not support type guards or, more general, effect system (cf. [Nielson99a]).

4.4. Generic and Parameterized Types

Some notes on terminology:

Type Parameter vs. Type Argument: A type parameter is a declaration containing type variables. A type argument is a binding of a type parameter to a concrete type or to another type parameter. Binding to another type parameter can further restrict the bounds of the type parameter.

This is similar to function declarations (with formal parameters) and function calls (with arguments).

4.4.1. Generic Types

A class declaration or interface declaration with type parameters declares a generic type. A generic type declares a family of types. The type parameters have to be bound with type arguments when referencing a generic type.

4.4.2. Type Variables

A type variable is an identifier used as a type in the context of a generic class definition, generic interface definition or generic method definition. A type variable is declared in a type parameter as follows.

Syntax

TypeVariable:
	(declaredCovariant?='out' | declaredContravariant?='in')?
	name=IdentifierOrThis ('extends' declaredUpperBound=TypeRef)?
;

Example 8. Type Variable as Upper Bound

Note that type variables are also interpreted as types. Thus, the upper bound of a type variable may be a type variable as shown in the following snippet:

class G<T> {
    <X extends T> foo(x: X): void { }
}

Properties

A type parameter defines a type variable, which type may be constrained with an upper bound.

Properties of TypeVariable:

$n a m e$: Type variable, as type variable contains only an identifier, we use type parameter instead of type variable (and vice versa) if the correct element is clear from the context.
$d e c l a r e d U p p e r B o u n d$: Upper bound of the concrete type being bound to this type variable, i.e. a super class.

Semantics

Req. IDE-10: Type Variable Semantics (ver. 1)

Enum is not a valid metatype in $d e c l a r e d U p p e r B o u n d s$ .
Wildcards are not valid in $d e c l a r e d U p p e r B o u n d s$ .
Primitives are not valid in $d e c l a r e d U p p e r B o u n d s$ .
Type variables are valid in $d e c l a r e d U p p e r B o u n d s$ .

A type variable can be used in any type expression contained in the generic class, generic interface, or generic function / method definition.

Example 9. F bounded quantification

Using a type variable in the upper bound reference may lead to recursive definition.

class Chain<C extends Chain<C, T>, T> {
    next() : C { return null; }
    m() : T { return null; }
}

Type Inference

In many cases, type variables are not directly used in subtype relations as they are substituted with the concrete types specified by some type arguments. In these cases, the ordinary subtype rules apply without change. However, there are other cases in which type variables cannot be substituted:

Inside a generic declaration.
If the generic type is used as raw type.
If a generic function / method is called without type arguments and without the possibility to infer the type from the context.

In these cases, an unbound type variable may appear on one or both sides of a subtype relation and we require subtype rules that take type variables into account.

It is important to note that while type variables may have a declared upper bound, they cannot be simply replaced with that upper bound and treated like existential types. The following example illustrates this:

Example 10. Type variables vs. existential types

class A {}
class B extends A {}
class C extends B {}

class G<T> {}

class X<T extends A, S extends B> {

    m(): void {

        // plain type variables:
        var t: T;
        var s: S;

        t = s;  // ERROR: "S is not a subtype of T." at "s" (1)

        // existential types:
        var ga: G<? extends A>;
        var gb: G<? extends B>;

        ga = gb;  (2)
    }
}

1	Even though the upper bound of `S` is a subtype of `T`’s upper bound (since $B < : A$ ), we cannot infer that `S` is a subtype of `T`, because there are valid concrete bindings for which this would not be true: for example, if `T` were bound to `C` and `S` to `B`.
2	This differs from existential types (see `ga` and `gb` and line 21): `G<? extends B>` $< :$ `G<? extends A>` ).

We thus have to define subtype rules for type variables, taking the declared upper bound into account. If we have a subtype relation in which a type variable appears on one or both sides, we distinguish the following cases:

If we have type variables on both sides: the result is true if and only if there is the identical type variable on both sides.
If we have a type variable on the left side and no type variable on the right side:
the result is true if and only if the type variable on the left has one or more declared upper bounds.
$i n t e r s e c t i o n (l e f t . d e c l a r e d U p p e r B o u n d s) < : r i g h t$
This is the case for

$(T e x t e n d s B) < : A$

in which T is an unbound type variable and A, B two classes with $B < : A$ .
In all other cases the result is false.
This includes cases such as

$B < : (T e x t e n d s A)$

which is always false, even if $B < : A$ or

$(T e x t e n d s A) < : (S e x t e n d s B)$

which is always false, even if $A = B$ .

We thus obtain the following defintion:

Definition: Subtype Relation for Type Variables

For two types $T, S$ of which at least one is a type variable, we define

if both T and $S$ are type variables:

$\frac{T = S}{T < : S}$
if T is a type variable and $S$ is not:

$\frac{T . d e c l a r e d U p p e r B o u n d s . s i z e > 0 \land \forall t \in T . d e c l a r e d U p p e r B o u n d s : t < : S}{T < : S}$

4.4.3. Parameterized Types

References to generic types (cf. Classes) can be parameterized with type arguments. A type reference with type arguments is called parameterized type.

Syntax

ParameterizedTypeRef:
    ParameterizedTypeRefNominal | ParameterizedTypeRefStructural;

ParameterizedTypeRefNominal:
    declaredType=[Type|TypeReferenceName]
    (=> '<' typeArgs+=TypeArgument (',' typeArgs+=TypeArgument)* '>')?;

ParameterizedTypeRefStructural:
    definedTypingStrategy=TypingStrategyUseSiteOperator
    declaredType=[Type|TypeReferenceName]
    (=>'<' typeArgs+=TypeArgument (',' typeArgs+=TypeArgument)* '>')?
    ('with' TStructMemberList)?;

TypeArgument returns TypeArgument:
    Wildcard | TypeRef;

Wildcard returns Wildcard:
    '?'
    (
          'extends' declaredUpperBound=TypeRef
        | 'super' declaredLowerBound=TypeRef
    )?
;

Properties

Properties of parameterized type references (nominal or structural):

declaredType: Referenced type by type reference name (either the simple name or a qualified name, e.g. in case of namespace imports).
typeArgs: The type arguments, may be empty.
definedTypingStrategy: Typing strategy, by default nominal, see Structural Typing for details
structuralMembers: in case of structural typing, reference can add additional members to the structural type, see Structural Typing for details.

Pseudo Properties:

importSpec: The ImportSpecifier, may be null if this is a local type reference. Note that this may be a NamedImportSpecifier. See Import Statement for details for details.
moduleWideName: Returns simple name of type, that is either the simple name as declared, or the alias in case of an imported type with alias in the import statement.

Semantics

The main purpose of a parameterized type reference is to simply refer to the declared type. If the declared type is a generic type, the parameterized type references defines a substitution of the type parameters of a generic type with actual type arguments. A type argument can either be a concrete type, a wildcard or a type variable declared in the surrounding generic declaration. The actual type arguments must conform to the type parameters so that code referencing the generic type parameters is still valid.

Req. IDE-11: Parameterized Types (ver. 1)

For a given parameterized type reference $R$ with $G = R . d e c l a r e d T y p e$ , the following constraints must hold:

The actual type arguments must conform to the type parameters, that is:

$| G . t y p e P a r s | = | R . t y p e A r g s |$
$\land \forall i, 0 < i < | R . t y p e A r g s | : [[R . t y p e A r g s_{i}]] < : [[R . t y p e P a r s_{i}]]$

We define type erasure similar to Java [Gosling12a(p.S4.6)] as 'mapping from types (possibly including parameterized types and type variables) to types (that are never parameterized types or type variables)'. We write $T$ ^o for the erasure of type T.^[11]

Definition: Parameterized Type

A parameterized type reference $R$ defines a parameterized type T, in which all type parameters of $R . d e c l a r e d T y p e$ are substituted with the actual values of the type arguments. We call the type $T^{0}$ , in which all type parameters of $R . d e c l a r e d T y p e$ are ignored, the raw type or erasure of T.

We define for types in general:

The erasure $G$ ^o of a parameterized type $G < T_{1}, . . ., T_{n} >$ is simply $G$ .
The erasure of a type variable is the erasure of its upper bound.
The erasure of any other type is the type itself.

This concept of type erasure is purely defined for specification purposes. It is not to be confused with the real type erasure which takes place at runtime, in which almost no types (except primitive types) are available.

That is, the type reference in var G<string> gs; actually defines a type G<string>, so that $[[g s]] = G < string >$ . It may reference a type defined by a class declaration class G<T>. It is important that the type G<string> is different from G<T>.

If a parameterized type reference $R$ has no type arguments, then it is similar to the declared type. That is, $[[R]] = T = R . d e c l a r e d T y p e$ if (and only if) $| R . t y p e A r g s | = 0$ .

In the following, we do not distinguish between parameter type reference and parameter type – they are both two sides of the same coin.

Example 11. Raw Types

In Java, due to backward compatibility (generics were only introduced in Java 1.5), it is possible to use raw types in which we refer to a generic type without specifying any type arguments. This is not possible in N4JS, as there is no unique interpretation of the type in that case as shown in the following example. Given the following declarations:

class A{}
class B extends A{}
class G<T extends A> { t: T; }
var g: G;

In this case, variable g refers to the raw type G. This is forbidden in N4JS, because two interpretations are possible:

g is of type G<? extends>
g is of type G<A>

In the first case, an existential type would be created, and g.t = new A(); must fail.

In the second case, g = new G<B>(); must fail.

In Java, both assignments work with raw types, which is not really safe. To avoid problems due to different interpretations, usage of raw types is not allowed in N4JS. ^[12]

Calls to generic functions and methods can also be parameterized, this is described in Function Calls. Note that invocation of generic functions or methods does not need to be parameterized.

Definition: Type Conformance

We define type conformance for non-primitive type references as follows:

For two non-parameterized types $T^{0}$ and $S^{0}$ ,

$\frac{S^{0} \in T^{0} . s u p^{*} \cup T^{0} . i n t e r f a c e s^{*}}{T^{0} < : S^{0}}$
For two parameterized types $T < T_{1}, . . ., T_{n} >$ and $S < S_{1}, . . ., S_{m} >$

$\frac{T^{0} < : S^{0}}{T < : S}$
$(n = 0 \lor m = 0 \lor (n = m \to \forall i :$
$T_{i} . u p p e r B o u n d < : S_{i} . u p p e r B o u n d$
$\land T_{i} . l o w e r B o u n d : > S_{i} . l o w e r B o u n d))}$

Example 12. Subtyping with parameterized types

Let classes A, B, and C are defined as in the chapter beginning ( $C < : B < : A$ ). The following subtype relations are evaluated as indicated:

G<A> <: G<B>                        -> false
G<B> <: G<A>                        -> false
G<A> <: G<A>                        -> true
G<A> <: G<?>                        -> true
G<? extends A> <: G<? extends A>    -> true
G<? super A> <: G<? super A>        -> true
G<? extends A> <: G<? extends B>    -> false
G<? extends B> <: G<? extends A>    -> true
G<? super A> <: G<? super B>        -> true
G<? super B> <: G<? super A>        -> false
G<? extends A> <: G<A>              -> false
G<A> <: G<? extends A>              -> true
G<? super A> <: G<A>                -> false
G<A> <: G<? super A>                -> true
G<? super A> <: G<? extends A>      -> false
G<? extends A> <: G<? super A>      -> false
G<?> <: G<? super A>                -> false
G<? super A> <: G<?>                -> true
G<?> <: G<? extends A>              -> false
G<? extends A> <: G<?>              -> true

The figure Cheat Sheet: Subtype Relation of Parameterized Types shows the subtype relations of parameterized types (of a single generic type), which can be used as a cheat sheet.

Figure 3. Cheat Sheet: Subtype Relation of Parameterized Types

Example 13. Subtyping between different generic types

Let classes $G$ and $H$ be two generic classes where:

class G<T> {}
class H<T> extends G<T> {}

Given a simple, non-parameterized class A, the following subtype relations are evaluated as indicated:

G<A> <: G<A>                        -> true
H<A> <: G<A>                        -> true
G<A> <: H<A>                        -> false

Type Inference

Type inference for parameterized types uses the concept of existential types (in Java, a slightly modified version called capture conversion is implemented).

The general concept for checking type conformance and inferring types for generic and parameterized types is described in [Igarashi01a] for Featherweight Java with Generics.

The concept of existential types with wildcard capture (a special kind of existential type) is published in [Torgersen05a], further developed in [Cameron08b] (further developed in [Cameron09a] [Summers10a], also see [Wehr08a] for a similar approach). The key feature of the Java generic wildcard handling is called capture conversion, described in [Gosling12a(p.S5.1.10)]. However, there are some slight differences to Java 6 and 7, only with Java 8 similar results can be expected. All these papers include formal proofs of certain aspects, however even these paper lack proof of other aspect

The idea is quite simple: All unbound wildcards are replaced with freshly created new types ^[13], fulfilling the constraints defined by the wildcard’s upper and lower bound. These newly created types are then handled similar to real types during type inference and type conformance validation.

Example 14. Existential Type

The inferred type of a variable declared as

var x: G<? extends A>;,

that is the parameterized type, is an existential type $E_{1}$ , which is a subtype of A. If you have another variable declared as

var y: G<? extends A>;

another type $E_{2}$ is created, which is also a subtype of A. Note that $E_{1} \neq E_{2}$ ! Assuming typical setter or getter in G, e.g. set(T t) and T get(), the following code snippet will produce an error:

y.set(x.get())

This is no surprise, as x.get() actually returns a type $E_{1}$ , which is not a subtype of $E_{2}$ .

The upper and lower bound declarations are, of course, still available during type inference for these existential types. This enables the type inferencer to calculate the join and meet of parameterized types as well.

Req. IDE-12: Join of Parameterized Types (ver. 1)

The join of two parameterized types $G < T_{1}, . . ., T_{n} >$ and $H < S_{1}, . . ., S_{m} >$ is the join of the raw types, this join is then parameterized with the join of the upper bounds of of type arguments and the meet of the lower bounds of the type arguments.

For all type rules, we assume that the upper and lower bounds of a non-generic type, including type variables, simply equal the type itself, that is for a given type T, the following constraints hold:
$u p p e r (T) = l o w e r (T) = T$

Example 15. Upper and lower bound of parameterized types

Assuming the given classes listed above, the following upper and lower bounds are expected:

G<A>            -> upperBound = lowerBound = A
G<? extends A>  -> lowerBound = null, upperBound = A
G<? super A>    -> lowerBound = A, upperBound = any
G<?>            -> lowerBound = null, upperBound = any

This leads to the following expected subtype relations:

(? extends A) <: A  -> true
(? super A) <: A    -> false
A <: (? extends A)  -> false
A <: (? super A)    -> true

Note that there is a slight difference to Java: In N4JS it is not possible to use a generic type in a raw fashion, that is to say without specifying any type arguments. In Java, this is possible due to backwards compatibility with early Java versions in which no generics were supported.

In case an upper bound of a type variable shall consist only of a few members, it seems convenient to use additional structural members, like on interface I2 in the example Use declared interfaces for lower bounds below. However, type variables must not be constrained using structural types (see constraint [Req-IDE-76]). Hence, the recommended solution is to use an explicitly declared interface that uses definition site structural typing for these constraints as an upper bound (see interface in Use declared interfaces for lower bounds).

Example 16. Use declared interfaces for lower bounds

interface I1<T extends any with {prop : int}> { // error
}

interface ~J {
    prop : int;
}
interface I2<T extends J> {
}

4.5. Primitive ECMAScript Types

N4JS provides the same basic types as ECMAScript [ECMA11a(p.p.28)].

In ECMAScript, basic types come in two flavors: as primitive types [ECMA11a(p.S8Types, p.p.28)] and as Objects [ECMA11a(p.S15, p.p.102)]. In N4JS, primitive types are written with lower cases, object types with first case capitalized. For example, String is the primitive ECMAScript string type, while String is an object.

The following ECMAScript primitive types are supported, they are written with lower case letters::

undefined: [ECMA11a(p.S8.3)]; cannot be used in type expression, see void below.
null [ECMA11a(p.S8.3)]; cannot be used in type expression
boolean [ECMA11a(p.S8.3)]
string [ECMA11a(p.S8.4)]
number [ECMA11a(p.S8.5)]

Although Object is a primitive type in [ECMA11a(p.S8.5)], it is interpreted here as an object type and described in Object Type.

Please note that primitive types are values (= no objects) so they have no properties and you cannot inherit from them.

4.5.1. Undefined Type

As a built-in type, the type undefined cannot be declared explicitly by the user by means of a type expression. Note in ECMAScript there are three distinct use cases of undefined:

undefined as type (as used here)
undefined as value (the only value of the undefined type)
undefined is a property of the global object with undefined (value) as initial value. Since ECMAScript 5 it is not allowed to reassign this property but this is not enforced by all ECMAScript/JavaScript engines.

The type undefined will be inferred to false in a boolean expression. It is important to note that something that is not assigned to a value is undefined but not null.

The type undefined is a subtype of all types. That is,

\frac{}{Γ ⊢ undefined < : T}

is an axiom and true for all types T.

Whenever an expression E has an inferred type of undefined, which means it will always evaluate to value undefined at runtime, a warning is shown, unless E is …

a void expression
the direct child expression of a void expression,
the direct child expression of an expression statement,
the undefined literal (i.e. the literal representing the undefined value),
the this literal.

4.5.2. Null Type

The null type cannot be declared explicitly by the user. Only the keyword null is inferred to type null.

Semantics

In contrast to undefined, it expresses the intentional absence of a value.

The null type can be assigned to any other type. That is, the type null is a subtype of all other types except undefined:

\frac{r i g h t \neq undefined}{Γ ⊢ null l e f t < : Type r i g h t}

Please note that

null==undefined evaluates to true
null===undefined evaluates to false
typeof null evaluates to object

Only the null keyword is inferred to type null. If null is assigned to a variable, the type of the variable is not changed. This is true, in particular, for variable declarations. For example in

var x = null;

the type of variable x is inferred to any (cf. Variable Statement).

The type null will be inferred to false in a boolean expression.

The call typeof null will return ’object’.

4.5.3. Primitive Boolean Type

Represents a logical entity having two values, true and false.

Please note that a boolean primitive is coerced to a number in a comparison operation so that

Source Result

Source	Result
`var a = true; console.log(a == 1)`	prints true
`var b = false; console.log(b == 0)`	prints true

var a = true; console.log(a == 1)

prints true

var b = false; console.log(b == 0)

prints true

Semantics

The type boolean is subtype of any:

\frac{}{boolean < : any}

Variables of type boolean can be auto-converted (coerced) to Boolean, as described in Autoboxing and Coercing.

4.5.4. Primitive String Type

A finite sequence of zero or more 16-bit unsigned integer values (elements). Each element is considered to be a single UTF-16 code unit.

Also string as primitive type has no properties, you can access the properties available on the object String as string will be coerced to String on the fly but just for that property call, the original variable keeps its type:

var a = "MyString"
console.log(typeof a) // string
console.log(a.length) // 8
console.log(typeof a) // string

You can handle a primitive string like an object type String but with these exceptions:

typeof "MyString" is 'string' but typeof new String("MyString") is 'object'
"MyString" instanceof String or instanceof Object will return false, for new String("MyString") both checks evaluate to true
console.log(eval("2+2")) returns 4, console.log(eval(new String("2+2"))) returns string "2+2"

This marks a difference to Java. In JavaScript, Unicode escape sequences are never interpreted as a special character.

Semantics

The string type is a subtype of any:

\frac{}{string < : any}

It is supertype of the N4JS primitive type pathselector, typeName and i18nKey. Primitive Pathselector and I18nKey

However, variables of type string can be auto-converted (coerced) to string, as described in Autoboxing and Coercing.

4.5.5. Primitive Number Type

In ECMAScript numbers are usually 64-bit floating point numbers. For details see [ECMA11a(p.8.5)]. The prefix 0 indicates that the number is octal-based and the prefix 0x marks it as hexadecimal-based.

NaN can be produced by e.g. ‘0 / 0’' or ‘1 - x’. typeof NaN will return number.

Semantics

The type number is subtype of any:

\frac{}{number < : any}

However, variables of type number can be auto-converted (coerced) to Number, as described in Integer Literals .

4.5.6. Primitive Type int

Actually ECMAScript defines an internal type int32. A number of this type is returned by the binary or operation using zero as operand, e.g. ECMAScript’s internal type int32 can be represented in N4JS by a built-in primitive type called int. For details on how numeric literals map to types number and int, refer to Integer Literals.

for the time being, built-in type int is synonymous to type number. This means one can be assigned to the other and a value declared to be of type int may actually be a 64-bit floating point number.^[14]

4.5.7. Primitive Symbol Type

The primitive type symbol is directly as in ECMAScript 6. Support for symbols is kept to a minimum in N4JS. While this primitive type can be used without any restrictions, the only value of this type available in N4JS is the built-in symbol Symbol.iterator. Other built-in symbols from ECMAScript 6 and the creation of new symbols are not supported. For more details, see Symbol.

4.6. Primitive N4JS Types

Additionally to the primitive ECMAScript types, the following N4JS-specific primitive types are supported:

any: enables ECMAScript-like untyped variable declarations
void: almost similar to undefined, except it can be used as a return type of functions and methods
unknown: inferred in case of a type inference error
pathSelector<T>, i18nKey: subtypes of string

4.6.1. Any Type

Any type is the default type of all variables for without a type declaration. It has no properties. A value of any other type can be assigned to a variable of type any, but a variable declared any can only be assigned to another variable declared with the type any.

4.6.1.1. Semantics

any is supertype of all other types. That is,

\frac{}{Γ ⊢ Type l e f t < : a n y}

is an axiom and true for all types.

4.6.1.2. Type Inference

If a variable is explicitly declared as type any, the inferred type of that variable will always be any.

4.6.1.2.1. Default Type of Variables

If a type annotation is missing and no initializer is provided, then the type of a variable is implicitly set to any.

In that case, the inferred type of that variable will always be any as well. If an initializer is provided, the declared type of the variable will be set to the inferred type of the initializer. Therefore in the latter case, the inferred type of the variable will always be the type of the initializer (cf. Variable Statement).

If a variable is declared as type , it can be used just as every variable can be used in raw ECMAScript. Since every property can be get and set, the types of properties is inferred as as well. This is formally expressed in Identifier.

4.6.2. Void Type

The type void is used to denote that there is no value at all, as opposed to type undefined which denotes that there is a value, but it is always undefined.

The only valid use of type void is to declare that a function or method does not return anything. In particular, this means:

void is disallowed as type argument,
void is disallowed as upper/lower bound of type parameters and wild cards,
when used as return type of functions or methods, void may not be nested, i.e.
```
function foo(): void {}  // ok
function bar(): any|void {}  // error
```

In all the above disallowed cases, type undefined should be used instead of void.

4.6.2.1. Semantics

Req. IDE-13: Void Type (ver. 1)

The type void may only be used as the immediate return type of a function or method.
If a function $f$ is declared to return void, an error is created if a return statement contains an expression:

$f . r e t u r n T y p e = void \to$
$\forall r, μ (r) = ReturnStatement, r . c o n t a i n i n g F u n c t i o n = f : r . e x p r e s s i o n = null$
If a function $f$ is declared to return void, an error is issued if the function is called in any statement or expression but an expression statement directly:

$f . r e t u r n T y p e = void \to$
$\forall e, b i n d (e, f) : μ (e . c o n t a i n e r) = ExpressionStatement$

The following type hierarchy is defined: void is only a subtype of itself but not of any other type and no other type is a subtype of void.

\frac{}{void < : void}

Since void cannot be used as the type of variables, fields, formal parameters, etc., a function or method with a return type of void cannot be used on the right-hand side of an assignment or in the argument list of a call expression (note the difference to plain JavaScript).

The ECMAScript void operator (see Unary Expressions) has a type of undefined, not void, because it evaluates to value undefined and can be used on the right-hand side of assignments, etc.

4.6.3. Unknown Type

Internally N4JS defines the type unknown. This type cannot be used by the user. Instead, it is inferred in case of errors. unknown behaves almost similar to any+. However no error messages once a variable or expression has been inferred to unknown in order to avoid consequential errors.

4.6.4. Primitive Pathselector and I18nKey

N4JS introduces three new types which are subtypes of string. These types are, in fact, translated to strings and do not add any new functionality. They are solely defined for enabling additional validation.

pathSelector<T> is a generic type for specifying path selector expressions. PathSelectors are used to specify a path to a property in a (JSON-like) model tree.
The type variable T defines the context type (or type of the root of the tree) in which the selector is to be validated. A path selector is defined as a string literal that has to conform to the path selector grammar. The context type is then used to perform a semantic
i18nKey is a string which refers to an internationalization key. The i18nKey type is used to reference resource keys specified in resource files. In a project $p$ , the i18nKey type defines the transitive set of all resource keys accessible from $p$ . Since resource keys are specified as strings, this means that the i18nKey type defines a subset of all string literals that can be assigned to a variable of type i18nKey in the current project. That means that an assignment of a string literal to a variable of type i18nKey is only valid if that string literal is contained in the set defined by i18nKey. Resource keys are declared in the properties files of a project and all resource keys from a project are accessible to any project depending on it.

I18nkeys are not yet validated

4.6.4.1. Semantics

The N4JS primitive types pathSelector<T>, i18nKey and pathSelector<T> are basically only marker types of strings for enabling additional validation. Thus, they are completely interchangeable with string types:

$\frac{}{typeName < T > < : string} \frac{}{string < : typeName < T >}$
$\frac{}{i18nKey < : string} \frac{}{string < : i18nKey}$
$\frac{}{pathSelector < T > < : string} \frac{}{string < : pathSelector < T >}$

As special literals for these N4JS types do not exist, the type has to be explicitly specified in order to enable the additional validation. Note that this validation cannot be applied for more complicated expressions with parts which cannot be evaluated at compile time. For example, "some.path."segment".prop" cannot be evaluated at compile time.

4.7. Built-in ECMAScript Object Types

N4JS supports all built-in ECMAScript objects [ECMA11a(p.S15)], interpreted as classes. Some of these object types are object versions of primitive types. The object types have the same name as their corresponding primitive type, but start with an upper case letter.

The following types, derived from certain ECMAScript predefined objects and constructs, are supported by means of built-in types as they are required by certain expressions.

Object [ECMA11a(p.p.111)];
Function [ECMA11a(p.p.117)]; representing functions and function objects Function Type but also methods (Methods)
Array [ECMA11a(p.p.122)], representing array objects, see Array Object Type
String [ECMA11a(p.p.141)]
Boolean [ECMA11a(p.p.141)]
Number [ECMA11a(p.p.141)]
RegExp [ECMA11a(p.p.180)]; they can be constructed by means of special literals (cf. Literals)
global object type
Symbol
Promise
Iterator and Iterable

All other ECMAScript types ([ECMA11a(p.S15)], such as Math, Date, or Error are supported by means of predefined classes. ECMAScript 2015 types are defined in the ECMAScript 2015 runtime environment. Since they are defined and used similar to user defined classes, they are not explained in further detail here. These predefined objects are kind of subtypes of Object.

4.7.1. Semantics

It is not possible to inherit from any of the built-in ECMAScript object types except for Object and Error, that is, to use one of these types as supertype of a class. From the N4JS language’s point of view, these built-in types are all final.

4.7.2. Object Type

Object [ECMA11a(p.S8.6)] is the (implicit) supertype of all declared (i.e., non-primtive) types, including native types. It models the ECMAScript type Object, except that no properties may be dynamically added to it. In order to declare a variable to which properties can be dynamically added, the type Object+ has to be declared (cf. Type Modifiers).

4.7.3. Function-Object-Type

The built-in object type Function, a subtype of Object, represents all functions, regardless of how they are defined (either via function expression, function declaration, or method declaration). They are described in detail in Function-Object-Type.

Since Function is the supertype of all functions regardless of number and types of formal parameters, return type, and number and bounds of type parameters, it would not normally be possible to invoke an instance of Function. For the time being, however, an instance of Function can be invoked, any number of arguments may be provided and the invocation may be parameterized with any number of type arguments (which will be ignored), i.e. [Req-IDE-101] and [Req-IDE-102] do not apply.

4.7.4. Array Object Type

The Array type is generic with one type parameter, which is the item type. An array is accessed with the index operator, the type of the index parameter is Number. The type of the stored values is typeArgs[0] (cf. Array Literal). Due to type erasure, the item type is not available during runtime, that is to say there are no reflective methods returning the item type of an array.

Req. IDE-14: Array Type (ver. 1)

For an array type A, the following conditions must be true:

$| A . t y p e A r g s | = 1$

4.7.5. String Object Type

Object type version of string. It is highly recommend to use the primitive version only. Note that is is not possible to assign a primitive typed value to an object typed variable.

4.7.6. Boolean Object Type

Object type version of boolean. It is highly recommend to use the primitive version only. Note that is is not possible to assign a primitive typed value to an object typed variable.

4.7.7. Number Object Type

Object type version of number. It is highly recommend to use the primitive version only. Note that is is not possible to assign a primitive typed value to an object typed variable.

4.7.8. Global Object Type

This is the globally accessible namespace which contains element such as undefined, and in case of browsers, window. Depending on the runtime environment, the global object may has different properties defined by means of dynamic polyfills.

4.7.9. Symbol

The symbol constructor function of ECMAScript 2015. Support for symbols is kept to a minimum in N4JS:

creating symbols with var sym = Symbol("description") is not supported.
creating shared symbols with var sym = Symbol.for("key") is not supported. Also the inverse Symbol.keyFor(sym) is not supported.
retrieving built-in symbols via properties in Symbol is supported, however, the only built-in symbol available in N4JS is the iterator symbol that can be retrieved with Symbol.iterator.

The rationale for this selective support for symbols in N4JS is to allow for the use (and custom definition) of iterators and iterables and their application in the for…of loop with as little support for symbols as possible.

4.7.10. Promise

Promise is provided as a built-in type as in ECMAScript 2015. Also see Asynchronous Functions for asynchronous functions.

4.7.11. Iterator Interface

A structurally typed interface for iterators as defined by theECMAScript 6 iterator protocol.

Iterable in N4JS

// providedByRuntime
export public interface ~Iterator<T>  {
    public next(): IteratorEntry<T>
}

// providedByRuntime
export public interface ~IteratorEntry<T> {
    public done: boolean;
    public value: T?;
}

Interface IteratorEntry was introduced mainly as a workaround; this interface could be removed and replaced with a corresponding structural type reference as return type of method next()

4.7.12. Iterable Interface

A structurally typed interface for objects that can be iterated over, i.e. iterables as defined by the ECMAScript 6 iterator protocol.

// providedByRuntime
export public interface ~Iterable<T> {
    public [Symbol.iterator](): Iterator<T>
}

Note that this interface’s method is special in that a symbol is used as identifier. You can use the ordinary syntax for computed property names in ECMAScript 6 for overriding / implementing or invoking this method.

4.8. Built-In N4JS Types

N4JS additionally provides some built-in classes which are always available with the need to explicitly import them.

4.8.1. N4Object

Although N4Object is a built-in type, it is not the default supertype. It is a subtype of Object.

4.8.1.1. Semantics

\frac{}{N4Object < : Object}

4.8.2. N4Class

The type N4Class is used for extended reflection in N4JS.

Add further docs for this type

4.8.3. IterableN

Work in progress.

Currently there are built-in types Iterable2<T1,T2>…Iterable9<T1,…,T9>. They are mainly intended for type system support of array destructuring literals.

This is not documented in detail yet, because we want to gain experience with the current solution first, major refinement may be incoming.

4.9. Type Modifiers

Type expressions can be further described with type modifiers. The type modifiers add additional constraints to the type expression which are then used to perform a stricter validation of the source code. Type modifiers can not be used in type arguments.

The general type modifiers $n u l l a b l e$ , $n o n n u l l$ and $d y n a m i c$ can be used for variables, attributes, method parameters and method types. Optional and variadic modifiers can only be applied for formal parameters.

4.9.1. Dynamic

The dynamic type modifier marks a type as being dynamic. A dynamic type behaves like a normal JavaScript object, so you can read/write any property and call any method on it. The default behavior for a type is to be static, that is no new properties can be added and no unknown properties can be accessed.

T $< :$ T+ and T+ $< :$ T is always true. Using dynamically added members of a dynamic type is never type safe. Using the delete operator on a subtype of N4Object is not allowed.

Req. IDE-15: Non-Dynamic Primitive Types (ver. 1)

All primitive types except any must not be declared dynamic.
Only parameterized type references and this type reference can be declared dynamic.^[15]

4.9.2. Optional Return Types

Only formal parameters and return types can be marked as optional.

An optional return type indicates that the function / method need not be left via a return statement with an expression; in that case the return value is undefined. For constraints on using the optional modifier, see Function-Object-Type.

4.10. Union and Intersection Type (Composed Types)

Given two or more existing types, it is possible to compose a new type by forming either the union or intersection of the base types. The following example gives a small overview of common use cases of union and intersection types.

Example 17. Composed types

This example shows how union and intersection types affect the types of their field members in case the fields have different types. It is for illustration purposes only. The type of the composed field depends on the access type: When reading, the field type of an intersection/union also resolves to the intersection/union. In contrast, when writing a field, the field type of an intersection/union resolves to the union/intersection respectively.

interface A { f : int = 1; }
interface B { f : string = "h"; }

class CA implements A {}
class CB implements B {}

let aub : A|B; // union type
let aib : A&B; // intersection type

function u() {
    aub = (catIsAlive)? new CA() : new CB(); // catIsAlive is boolean
    let x = aub.f; // x = {1 | "h"}
    aub.f = undefined; // undefined can be assigned to int and string types
}
function i() {
    let a = aib as A;
    let b = aib as B;
    a.f = 23;
    b.f = "text";
    let x = aib.f; // x = {23 & "text"} which is impossible
}
// type of 'aub.f' --> int|string
let fu = aub.f;
// type of 'aub.f' --> int&string
aub.f = undefined;
// type of 'aib.f' --> int&string
let fi = aib.f;
// type of 'aib.f' --> int|string
aib.f = undefined;

Note that no instance aib of intersection type A&B can be instantiated, since the instance’s class would have to define a field f which would have to comply to both of the interfaces A and B. Still the function i() shows in general how variables of intersection types can be casted and accessed.

The following sections define these union and intersection types in detail.

4.10.1. Union Type

Union type reflect the dynamic nature of JavaScript. Union types can be used almost everywhere (e.g., in variable declarations or in formal method parameters). The type inferencer usually avoids returning union types and prefers single typed joins or meets. The most common use case for union types is for emulating method overloading, as we describe later on.^[16]

4.10.1.1. Syntax

For convenience, we repeat the definition of union type expression:

UnionTypeExpression: 'union' '{' typeRefs+=TypeRefWithoutModifiers (',' typeRefs+=TypeRefWithoutModifiers)* '}';

4.10.1.2. Semantics

An union type states that the type of a variable may be one or more types contained in the union type. In other words, a union type is a kind of type set, and the type of a variable is contained in the type set. Due to interfaces, a variable may conform to multiple types.

Req. IDE-18: Union Type (ver. 1)

For a given union type $U = u n i o n \{T_{1}, . . ., T_{n}\}$ , the following conditions must hold:

Non-empty: At least one element has to be specified:
$U . t y p e R e f s \neq \emptyset$ ( $n \geq 1)$
Non-dynamic: The union type itself must not be declared dynamic:
$\neg U . d y n a m i c$
Non-optional elements:
$\forall T \in U . t y p e R e f s \to \neg T . o p t$

Req. IDE-19: Union Type Subtyping Rules (ver. 1)

Let $U$ be an union type.

The union type is a common supertype of all its element types:

$\frac{T \in U . t y p e R e f s}{T < : U}$
More generally, a type is a subtype of a union type, if it is a subtype of at least one type contained in the union:

$\frac{\exists T \in U . t y p e R e f s : S < : T}{S < : U}$
A union type is a subtype of a type $S$ , if all types of the union are subtypes of that type. This rule is a generalization of the sub typing rules given in [Igarashi07a(p.p.40)]

$\frac{\forall T \in U . t y p e R e f s : T < : S}{U < : S}$
Commutativity: The order of element does not matter:

$u n i o n \{A, B\} = u n i o n \{B, A\}$
Associativity: $u n i o n \{A, u n i o n \{B, C\}\} = u n i o n \{u n i o n \{A, B\}, C\}$
Uniqueness of elements: A union type may not contain duplicates (similar to sets):

$\forall 1 \leq i < k \leq n, u n i o n \{T_{1}, . . ., T_{n}\} : T_{i} \neq T_{k}$

Req. IDE-20: Implicit simplification of union types (ver. 1)

Let $U$ be an union type. The following simplification rules are always automatically applied to union types.

Simplification of union type with one element: If a union type contains only one element, it is reduced to the element:

$\frac{u n i o n \{T\}}{T}$
Simplification of union types of union types: A union type $U$ containing another union type $V$ is reduced to a single union type $W$ , with $W . t y p e R e f s = U . t y p e R e f s \cup V . t y p e R e f s$ :

$\frac{u n i o n \{S_{1}, . . ., S_{k - 1}, u n i o n \{T_{1}, . . ., T_{m}\}, S_{k + 1}, . . ., S_{n}\}}{u n i o n \{S_{1}, . . ., S_{k - 1}, T_{1}, . . ., T_{m}, S_{k + 1}, . . ., S_{n}\}}$
Simplification of union type with undefined or null: Since undefined is the bottom type, and null is kind of a second button type, they are removed from the union:

$\frac{u n i o n \{T_{1}, . . ., T_{k - 1}, T_{k}, . . ., T_{n}\}}{u n i o n \{T_{1}, . . ., T_{k - 1}, u n d e f i n e d\}, T_{k}, . . ., T_{n}}$
$\frac{u n i o n \{T_{1}, . . ., T_{k - 1}, T_{k}, . . ., T_{n}\}}{u n i o n \{T_{1}, . . ., T_{k - 1}, n u l l\}, T_{k}, . . ., T_{n}}$

Simplification rules for union types with one element are applied first.

The structural typing strategy is propagated to the types of the union:

$\frac{~ u n i o n \{T_{1}, . . ., T_{n}\}}{u n i o n \{~ T_{1}, \dots, ~ T_{n}\}}$

Remarks:

The simplification rules may be applied recursively.
For given types $B < : A$ , and the union type $U = u n i o n \{A, B\}$ , $U \neq B$ . The types are equivalent, however: $A < : = U$ and $U < : = A$ .^[17]

Example 18. Subtyping with union type

Let A, B, and C be defined as in the chapter beginning ( $C < : B < : A$ )

The following subtyping relations with union types are to be evaluated as follows: ^[18]

A <: union{A}                                   -> true
A <: union{A,B}                                 -> true
B <: union{A,B}                                 -> true
C <: union{A,B}                                 -> true
A <: union{B,C}                                 -> false
B <: union{B,C}                                 -> true
C <: union{B,C}                                 -> true
union{A} <: A                                   -> true
union{B} <: A                                   -> true
union{B,C} <: A                                 -> true
union{A,B} <: B                                 -> false
union{X,Z} <: union{Z,X}                        -> true
union{X,Y} <: union{X,Y,Z}                      -> true
union{X,Y,Z} <: union{X,Y}                      -> false

The simplification constraints are used by the type inferrer. It may be useful, however, to define union types with superfluous elements, as the next example demonstrates

Example 19. Superfluous elements in union type

class A{}
class B extends A{}
class C extends A{}

function foo(p: union{A,B}) {..}

Although B is superfluous, it may indicate that the function handles parameters of type differently than one of type A or C.

Although a union type is a LCST of its contained (non-superfluous) types, the type inferrer usually does not create new union types when computing the join of types. If the join of types including at least one union type is calculated, the union type is preserved if possible. The same is true for meet.

For the definition of join and meet for union types, we define how a type is added to a union type:

Req. IDE-21: Union of union type (ver. 1)

The union of union types is defined similar to the union of sets. The union is not simplified, but it contains no duplicates.

If a type A is contained in a union type, then the union type is a common supertype, and (since it is the union itself) also the LCST of both types. This finding is the foundation of the definition of join of a (non-union) type with a union type:

Req. IDE-22: Join with Union Type (ver. 1)

The join $J$ of a union type $U$ with a type T is the union of both types:

\frac{J = U \cup T}{(U \lor T) = J}

Remarks:

Joining a union type with another type is not similar to joining the elements of the union type directly with another type. That is

$A j o i n u n i o n \{B, C\} \neq A j o i n B j o i n C$
The computed join is simplified according to the constraints defined above.

Req. IDE-23: Meet with Union Type (ver. 1)

The meet of union types is defined as the meet of the elements. That is

\begin{matrix} \frac{T_{1} \land S \land . . . \land T_{n} \land S}{u n i o n \{T_{1}, . . ., T_{n}\} \land S} \\ \frac{T_{1} \land S_{1}, . . ., T_{1} \land S_{m}, . . ., T_{n} \land S_{1}, . . ., T_{n} \land S_{m}}{u n i o n \{T_{1}, . . ., T_{n}\} \land u n i o n \{S_{1}, . . ., S_{m}\}} \end{matrix}

Remarks:

The meet of a union type with another type is not a union type itself. This gets clear when looking at the definition of meet and union type. While for a given $U = u n i o n \{A, B\}$ , $A < : U$ and $B < : U$ , the opposite $U < : A$ is usually not true (unless $U$ can be simplified to A). So, for $A \land U$ , usually $U$ cannot be the meet.

Req. IDE-24: Upper and Lower Bound of a Union Type (ver. 1)

The upper and lower bound of a union type $U$ is a union type $U^{'}$ containing the upper and lower bound of the elements of $U$ :

\begin{matrix} u p p e r (u n i o n \{T_{1}, . . ., T_{n}\}) : = u n i o n \{u p p e r (T_{1}), . . ., u p p e r (T_{1})\} \\ l o w e r (u n i o n \{T_{1}, . . ., T_{n}\}) : = u n i o n \{l o w e r (T_{1}), . . ., l o w e r (T_{1})\} \end{matrix}

4.10.1.3. Warnings

In case the any type is used in a union type, all other types in the union type definition become obsolete. However, defining other typers along with the any type might seem reasonable in case those other types are treated specifically and thus are mentioned explicitly in the definition. Nevertheless the use of the any type produces a warning, since its use can indicate a misunderstanding of the union type concept and since documentation can also be done in a comment.

Req. IDE-25: Any type in union types (ver. 1)

No union type shall conatin an type:

∄ a n y \in U . t y p e R e f s

Similar to the documentary purpose of using specific classes along with the any type is the following case. When two types are used, one of them a subtype of the other, then this subtype is obsolete. Still it can be used for documentary purposes. However, a warning will be produced to indicate unecessary code. The warning is only produced when both of the types are either classes or interfaces, since e.g. structural types are supertypes of any classes or interfaces.

Req. IDE-26: Redundant subtypes in union types (ver. 1)

Union types shall not contain class or interface types which are a subtype of another class or interface type that also is contained in the union type.

\begin{matrix} ∄ T T \in U . t y p e R e f s : \exists T \in U . t y p e R e f s : \\ (T T < : T \land i s C l a s s O r I n t e r f a c e (T) \land i s C l a s s O r I n t e r f a c e (T T)) \end{matrix}

4.10.2. Intersection Type

Intersection type reflects the dynamic nature of JavaScript, similar to union type. As in Java, intersection type is used to define the type boundaries of type variables in type parameter definitions. They are inferred by the type inferencer for type checking (as a result of join or meet). In contrast to Java, however, intersection type can be declared explicitly by means of intersection type expression.^[19]

4.10.2.1. Syntax

For convenience, we repeat the definition of intersection type expression and of type variables in which intersection types can be defined as in Java:

InterSectionTypeExpression: 'intersection' '{' typeRefs+=TypeRefWithoutModifiers (',' typeRefs+=TypeRefWithoutModifiers)* '}';

TypeVariable:   name=IDENTIFIER ('extends' declaredUpperBounds+=ParameterizedTypeRefNominal ('&' declaredUpperBounds+=ParameterizedTypeRefNominal)*)?

4.10.2.2. Semantics

An intersection type may contain several interfaces but only one class. It virtually declares a subclass of this one class and implements all interfaces declared in the intersection type. If no class is declared in the intersection type, the intersection type virtually declares a subclass of an N4Object instead. This virtual subclass also explains why only one single class may be contained in the intersection.

Req. IDE-27: Intersection Type (ver. 1)

For a given intersection type $I$ , the following conditions must hold:

The intersection must contain at least one type:

$I . t y p e R e f s \neq \emptyset$
Only one nominally typed class must be contained in the intersection type:

$(\exists C \in I . t y p e R e f s : μ (C) = Class \land C . i s S t r u c t u r a l) \to ∄ T \in I . t y p e R e f s ∖ \{C\} : μ (T) = Class \land T . i s S t r u c t u r a l$

A warning is produced when more than one nominal class is contained in the intersection type, since only undefined (or null) can be assigned to a type reference of this type.
Non-optional elements:

$\forall T \in I . t y p e R e f s \to \neg T . o p t$
If the intersection contains multiple references to the same generic type, a warning is produced if only undefined (or null) can be assigned to a type reference of this type. There are some rare cases in which this does not happen. This is true if for all type arguments one of the following conditions hold:
- a type argument corresponding to a type parameter without def-site variance is a wildcard with an upper bound (use "extends" or no bound) or a type argument not defining an upper bound corresponds to a covariant (out) type parameter, and this constraint (IDE-27) holds for an intersection created from the upper bounds of the type argument (or the lower bound of the type parameter).
- a type argument is a wildcard with lower bounds (since Object would be a solution)

Definition of structural typing attributes see [Req-ID-78701].

The combination of intersection types and generics is a bit tricky. The following example demonstrates that:

Example 20. Intersection and generics

Given the following types:

class G<T> {
     private T: t
	set(t: T) { this.t = t;}
	get(): T { return this.t; }
}
class C { public y; }
class D { public x; }
interface I {}

We use the generic with the getter and setter here only to demonstrate co- and contra variance effects.

Let

let g1: G<C> & G<D>;

be a variable. We can only assign undefined to g1, since any other value would not be confirm to the intersection. If we for example would assign

let gc = new G<C>()
g1 = gc;

we would run into contra-variance problems:

gc.set(new C());

This would implicitly also set a C in g1, which would not be compatible with D. This would lead to a problem in the following lines:

let gd: G<D> = g1;
let d: D = gd.get();

This is the typical contra variance problem.

Similar problems arise even with structural types.

Note that in theory more warnings could be produced, in particular in combination with structural types (and the fact that N4JS classes must explicitly implement even structural interfaces). We omit these kind of warnings for two reasons:

performance
anticipated slight changes in semantics (e.g. we may remove the requirement of explicitly implementing structural interfaces)

Since problems caused by not instanceable type references will be detected by programmers before runtime anyway, we do not need to be strict here. They are merely convenience features and they do not affect the correctness of the type system.

Req. IDE-175: Intersection Type Subtyping Rules (ver. 1)

Let $I$ be an intersection type.

An intersection type is a subtype of another type, if at least one of its contained types is a subtype of that type: ^[20]

\frac{\exists T \in I . t y p e R e f s : T < : S}{I < : S}

A type is a subtype of an intersection type, if it is a subtype of all types contained in the intersection type: ^[21]

\frac{\forall T \in I . t y p e R e f s : S < : T}{S < : I}

Non-optional elements: $\forall T \in I . t y p e R e f s \to \neg T . o p t$

Req. IDE-28: Implicit simplification of intersection types (ver. 1)

Let $I$ be an intersection type. The following simplification rules are always automatically applied to intersection types.

The structural typing strategy is propagated to the types of the intersection:

$\frac{~ i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\}}{i n t e r s e c t i o n \{~ T_{1}, \dots, ~ T_{n}\}}$

These subtyping rules are similar to Ceylon. ^[22]

During validation, intersection types containing union or other intersection types may be inferred. In this case, the composed types are flattened. The aforementioned constraints must hold. We also implicitly use this representation in this specification.

Example 21. Subtyping with intersection type

Let A, B, and C be defined as in the chapter beginning ( $C < : B < : A$ )

The following subtyping relations with intersection types are to be evaluated as follows: ^[23]

A <: intersection{A}                            -> true
A <: intersection{A,A}                          -> true
intersection{A,X} <: A                          -> true
intersection{X,A} <: A                          -> true
A <: intersection{A,X}                          -> false
intersection{A,X} <: intersection{X,A}          -> true
H12 <: intersection{I1,I2}                      -> true
intersection{I1,I2} <: H12                      -> false
H1 <: intersection{I1,I2}                       -> false
H23 <: intersection{I1,I2}                      -> false
B <: intersection{A}                            -> true
intersection{I1,I2} <: I                        -> true
H12 <: intersection{I,I2}                       -> true
A <: intersection{A,Any}                        -> true
intersection{A,Any} <: A                        -> true

The join of intersection types is defined as the join of the elements. That is:

$\frac{T_{1} \lor S \lor . . . \lor T_{n} \lor S}{i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\} \lor S}$
$\frac{T_{1} \lor S_{1}, . . ., T_{1} \lor S_{m}, . . ., T_{n} \lor S_{1}, . . ., T_{n} \lor S_{m}}{i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\} \lor i n t e r s e c t i o n \{S_{1}, . . ., S_{m}\}}$

The meet of intersection types is defined over their elements. That is:

$\frac{i n t e r s e c t i o n \{T_{1} \land S, . . ., T_{n} \land S\}}{i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\} \land S}$
$\frac{i n t e r s e c t i o n \{T_{1} \land S_{1}, . . ., T_{1} \land S_{m}, . . ., T_{n} \land S_{1}, . . ., T_{n} \land S_{m}\}}{i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\} \land i n t e r s e c t i o n \{S_{1}, . . ., S_{m}\}}$

The upper and lower bound of an intersection type $I$ is a union type $I^{'}$ containing the upper and lower bound of the elements of $I$ :

$u p p e r (i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\}) : = i n t e r s e c t i o n \{u p p e r (T_{1}), . . ., u p p e r (T_{1})\}$
$l o w e r (i n t e r s e c t i o n \{T_{1}, . . ., T_{n}\}) : = i n t e r s e c t i o n \{l o w e r (T_{1}), . . ., l o w e r (T_{1})\}$

4.10.2.3. Warnings

Using any types in intersection types is obsolete since they do not change the resulting intersection type. E.g. the intersection type of A, B and any is equivialent to the intersection type of A and B. However, using the any type is no error because it can be seen as a neutral argument to the intersection. Nevertheless the use of the any type produces a warning, since its use can indicate a misunderstanding of the intersection type concept and since it always can be omitted.

Req. IDE-32: Any type in intersection types (ver. 1)

No intersection type shall contain an type:

$∄ a n y \in I . t y p e R e f s$

The use of the any type in an intersection type is similar to the following case. When two types are used, one of them a supertype of the other, then this supertype is obsolete. Hence, a warning will be produced to indicate unecessary code. The warning is only produced when both of the types are either classes or interfaces, since e.g. structural types are supertypes of any classes or interfaces.

Req. IDE-33: Redundant supertypes in intersection types (ver. 1)

Intersection types shall not contain class or interface types which are a supertype of another class or interface type that also is contained in the intersection type.

∄ T \in I . t y p e R e f s : \exists T T \in I . t y p e R e f s : (T T < : T \land i s C l a s s O r I n t e r f a c e (T) \land i s C l a s s O r I n t e r f a c e (T T))

4.10.3. Composed Types in Wildcards

Composed types may appear as the bound of a wildcard. The following constraints apply: ^[24]

Req. IDE-34: Composed Types as Bound of a Wildcard (ver. 1)

A composed type may appear as the upper or lower bound of a wildcard. In the covariant case, the following subtype relations apply:

union{ G<? extends A>, G<? extends B> }  \subtype  G<? extends union{A,B}>
G<? extends intersection{A,B}>  \subtype  intersection{ G<? extends A>, G<? extends B> }

In the contra variant case, the following subtype relations apply:

union{ G<? super A>, G<? super B> }  \subtype  G<? super intersection{A,B}>
G<? super union{A,B}>  \subtype  intersection{ G<? super A>, G<? super B> }

4.10.4. Property Access for Composed Types

It is possible to directly access properties of union and intersection types. The following sections define which properties are accessible.

4.10.4.1. Properties of Union Type

As an (oversimplified) rule of thumb, the properties of a union type $U = T_{1} | T_{2}$ are simply the intersection of the properties $U . p r o p e r t i e s = T_{1} . p r o p e r t i e s \cap T_{2} . p r o p e r t i e s$ . In other words, a property 'p' in the union type is the least common denominator of all 'p' in T_{1} and T_{2}. It is not quite that simple, however, as the question of "equality" with regards to properties has to be answered.

For a given union type $U = T_{1} | T_{2}$ , the following constraints for its members must hold:

$\forall a \in U . a t t r i b u t e s :$

\begin{matrix} \forall k \in \{1, 2\} : \exists a_{k} \in T_{k} . a t t r i b u t e s : a_{k} . a c c > p r i v a t e \\ \land a . a c c = m i n (a_{1} . a c c, a_{2} . a c c) \\ \land a . n a m e = a_{1} . n a m e = a_{2} . n a m e \\ \land a . t y p e R e f = a_{1} . t y p e R e f = a_{2} . t y p e R e f \end{matrix}

$\forall m \in U . m e t h o d s :$

$\exists m_{1} \in T_{1} . m e t h o d s, m_{2} \in T_{2} . m e t h o d s,$
$w i t h p = m . f p a r s \land p^{'} = m_{1} . f p a r s \land p " = m_{2} . f p a r s, W L O G | p^{'} | \leq | p " | :$

\begin{matrix} \forall k \in \{1, 2\} : m_{k} . a c c > p r i v a t e \\ \land m . a c c = m i n (m_{1} . a c c, m_{2} . a c c) \\ \land m . n a m e = m_{1} . n a m e = m_{2} . n a m e \\ \land m . t y p e R e f = m_{1} . t y p e R e f | m_{2} . t y p e R e f \\ \land \forall i < | p " | : p_{i} e x i s t s w i t h \\ p_{i} . n a m e = \{\begin{matrix} {p "}_{i} . n a m e & i \geq | p^{'} | \lor {p^{'}}_{i} . n a m e = {p "}_{i} . n a m e \\ {p^{'}}_{i} . n a m e + "_" + {p "}_{i} . n a m e & e l s e \end{matrix} \\ p_{i} . t y p e R e f = \{\begin{matrix} {p^{'}}_{i} . t y p e R e f & {p "}_{i} . t y p e R e f & i < | p^{'} | \\ {p^{'}}_{| p^{'} | - 1} . t y p e R e f & {p "}_{i} . t y p e R e f & i \geq | p^{'} | \land {p^{'}}_{| p^{'} | - 1} . v a r \\ {p "}_{i} . t y p e R e f & e l s e \end{matrix} \\ p_{i} . o p t = \{\begin{matrix} ({p^{'}}_{i} . o p t \land {p "}_{i} . o p t) & i < | p^{'} | \\ {p "}_{i} . o p t & e l s e \end{matrix} \\ p_{i} . v a r = \{\begin{matrix} {p^{'}}_{i} . v a r \land {p "}_{i} . v a r & i < | p^{'} | \land i = | p " | - 1 \\ {p "}_{i} . v a r & i \geq | p^{'} | \land i = | p " | - 1 \\ f a l s e & e l s e \end{matrix} \end{matrix}

$\land (l = | p^{'} | = | p " | \land \neg ({p^{'}}_{l} - 1 . o p t \land {p "}_{l - 1} . o p t) \land \exists v \in \{p'_{l} - 1, p "_{l} - 1\} v . v a r : p_{l} e x i s t s w i t h$
$p_{l} . n a m e = v . n a m e$
$p_{i} . t y p e R e f = v . t y p e R e f$
$p_{i} . o p t = t r u e$
$p_{i} . v a r = t r u e$

The following table shows how non-method members of union types are merged. The resulting member type depends on whether the member is being accessed during a read (R) or write (W) operation. The type of a field, of a getter or of the parameter of a setter is indicated in brackets.

Table 4. Merged Members of Unions
Members	S=T		S≠T
	R	W	R	W
field:S \| field:T	field:S		getter:S\|T	setter:S&T
getter:S \| getter:T	getter:S	-	getter:S\|T	-
setter:S \| setter:T	-	setter:S	-	setter:S&T
field:S \| getter:T	getter:S	-	getter:S\|T	-
field:S \| setter:T	-	setter:S	-	setter:S&T
getter:S \| setter:T	-	-	-	-

4.10.4.1.1. Remarks on union type’s members:

Fields of the same type are merged to a composed field with the same type. Fields of different types are merged to a getter and setter.
The return type of a composed getter is the union type of the return types of the merged getters.
The type of a composed setter is the intersection type of the types of the merged setters.
Fields can be combined with getters and/or setters:
- fields combined with getters allow read-access.
- non-const fields combined with setters allow write-access.
- non-const fields combined with getters and setters, i.e. each type has either a non-const field or both a getter and a setter of the given name, allow both read- and write-access.
  
  Again, types need not be identical; for read-access the union of the fields’ types and the getters’ return types is formed, for write-access the intersection of the fields’ types and the setters’ types is formed. In the third case above, types are combined independently for read- and write-access if the getters and setters have different types.
The name of a method’s parameter is only used for error or warning messages and cannot be referenced otherwise.
The return type of a composed method is the union type of the return types of the merged methods.
A composed method parameter’s type is the intersection type of the merged parameters types.

4.10.4.2. Properties of Intersection Type

As an (oversimplified) rule of thumb, the properties of an intersection type $I = T_{1} & T_{2}$ are the union of properties $I . p r o p e r t i e s = T_{1} . p r o p e r t i e s \cup T_{2} . p r o p e r t i e s$ . In other words, a property 'p' in the union type is the greates common denominator of all 'p' in T_{1} and T_{2}. It is not quite that simple, however, as the question of "equality” with regards to properties has to be answered.

Req. IDE-36: Members of an Intersection Type (ver. 1)

For a given intersection type $I = T_{1} & T_{2}$ , the following constraints for its members must hold:

$\forall a \in I . a t t r i b u t e s :$

\begin{matrix} (\exists a_{1} \in T_{1} . a t t r i b u t e s, a_{1} . a c c > p r i v a t e) \lor (\exists a_{2} \in T_{2} . a t t r i b u t e s, a_{2} . a c c > p r i v a t e) \\ \land a . n a m e = \{\begin{matrix} a_{1} . n a m e & a_{1} \neq n u l l \land (a_{2} = n u l l \lor a_{2} . n a m e = a_{1} . n a m e) \\ a_{2} . n a m e & e l s e \end{matrix} \\ \land a . a c c = \{\begin{matrix} a_{1} . a c c & a_{1} \neq n u l l \land (a_{2} = n u l l \lor a_{2} . a c c \leq a_{1} . a c c) \\ a_{2} . a c c & e l s e \end{matrix} \\ \land a . t y p e R e f = \{\begin{matrix} a_{1} . t y p e R e f & a_{2} . t y p e R e f & a_{1} \neq n u l l \land a_{2} \neq n u l l \\ a_{1} . t y p e R e f & a_{1} \neq n u l l \\ a_{2} . t y p e R e f & e l s e (a_{2} \neq n u l l) \end{matrix} \end{matrix}

$\forall m \in I . m e t h o d s$ :

$(\exists m_{1} \in T_{1} . m e t h o d s, m_{1} . a c c > p r i v a t e) \lor (\exists m_{2} \in T_{1} . m e t h o d s, m_{2} . a c c > p r i v a t e) :$

\begin{matrix} w i t h p = m . f p a r s \\ \land i f m_{1} e x i s t s p^{'} = m_{1} . f p a r s (e l s e p^{'} = \emptyset), \\ \land i f m_{2} e x i s t s p " = m_{2} . f p a r s (e l s e p " = \emptyset), W L O G | p^{'} | \leq | p " | : \\ m . n a m e = \{\begin{matrix} m_{1} . n a m e & m_{1} \neq n u l l \land (m_{2} = n u l l \lor m_{2} . n a m e = m_{1} . n a m e) \\ m_{2} . n a m e & e l s e \end{matrix} \\ \land m . a c c = \{\begin{matrix} m_{1} . a c c & m_{1} \neq n u l l \land (m_{2} = n u l l \lor m_{2} . a c c \leq m_{1} . a c c) \\ m_{2} . a c c & e l s e \end{matrix} \\ \land m . t y p e R e f = \{\begin{matrix} m_{1} . t y p e R e f & m_{2} . t y p e R e f & m_{1} \neq n u l l \land m_{2} \neq n u l l \\ m_{1} . t y p e R e f & m_{1} \neq n u l l \\ m_{2} . t y p e R e f & e l s e (m_{2} \neq n u l l) \end{matrix} \\ \land \forall i < | p " | : p_{i} e x i s t s w i t h \\ p_{i} . n a m e = \{\begin{matrix} {p "}_{i} . n a m e & i \geq | p^{'} | \lor {p "}_{i} . n a m e = {p^{'}}_{i} . n a m e \\ {p^{'}}_{i} . n a m e + "_" + {p "}_{i} . n a m e & e l s e \end{matrix} \\ p_{i} . t y p e R e f = \{\begin{matrix} {p^{'}}_{i} . t y p e R e f | {p "}_{i} . t y p e R e f & i < | p^{'} | \\ {p^{'}}_{| p^{'} | - 1} . t y p e R e f | {p "}_{i} . t y p e R e f & i \geq | p^{'} | \land {p^{'}}_{| p^{'} | - 1} . v a r \\ {p "}_{i} . t y p e R e f & e l s e \end{matrix} \\ p_{i} . o p t = (\exists k \leq m i n (| p^{'} | - 1, i) : p'_{k} . o p t) \lor (\exists k \leq i : p "_{k} . o p t) \\ p_{i} . v a r = \{\begin{matrix} p_{i} . o p t \lor ({p^{'}}_{i} . v a r \lor {p "}_{i} . v a r) & i < | p^{'} | \land i = | p " | - 1 \\ {p "}_{i} . v a r & i \geq | p^{'} | \land i = | p " | - 1 \\ f a l s e & e l s e \end{matrix} \end{matrix}

$\land (l = | p^{'} | = | p " | \land l > 0 \land \neg (p_{l - 1} . o p t) \land \exists v \in \{p'_{l - 1}, p "_{l - 1}\} v . v a r : p_{l} e x i s t s w i t h$
$p_{l} . n a m e = v . n a m e$
$p_{i} . t y p e R e f = v . t y p e R e f$
$p_{i} . o p t = t r u e$
$p_{i} . v a r = t r u e$

The following table shows how non-method members of intersection types are merged. The resulting member type depends on whether the member is being accessed during a read (R) or write (W) operation. The type of a field, of a getter or of the parameter of a setter is indicated in brackets.

Table 5. Merged Members of Intersections
Members	S=T		S≠T
	R	W	R	W
field:S & field:T	field:S		getter:S&T	setter:S\|T
getter:S & getter:T	getter:S	-	getter:S&T	-
setter:S & setter:T	-	setter:S	-	setter:S\|T
field:S & getter:T	field:S		getter:S&T	setter:S
field:S & setter:T	field:S		getter:S	setter:S\|T
getter:S & setter:T	field:S		getter:S	setter:T

4.10.4.2.1. Remarks on intersection type’s methods:

The name of a method’s parameter is only used for error or warning messages and cannot be referenced otherwise.
The return type of a method is the intersection type of the return types of the merged methods.
A method parameter’s type is the union type of the merged parameters types.

4.11. Constructor and Classifier Type

A class definition as described in Classes declares types. Often, it is necessary to access these types directly, for example to access staticmembers or for dynamic construction of instances. These two use cases are actually slightly different and N4JS provides two different types, one for each use case: constructor and classifier type.^[25] The constructor is basically the classifier type with the additional possibility to call it via new in order to create new instances of the declared type.

Both meta types are different from Java’s type Class<T>, as the latter has a defined set of members, while the N4JS metatypes will have members according to a class definition. The concept of constructors as metatypes is similar to ECMAScript 2015 [ECMA15a(p.14.5)].

4.11.1. Syntax

ConstructorTypeRef returns ConstructorTypeRef: 'constructor' '{' typeArg = [TypeArgument] '}';

ClassifierTypeRef returns ClassifierTypeRef: 'type' '{' typeArg = [TypeRef] '}';

4.11.2. Semantics

Static members of a type T are actually members of the classifier type type{T}.
The keyword this in a static method of a type T actually binds to the classifier type type{T}.
The constructor type constructor{T} is a subtype of the classifier type type{T}:

$\forall T : c o n s t r u c t o r \{T\} < : t y p e \{T\}$
If a class B is a subtype (subclass) of a class A, then the classifier type type{B} also is a subtype of type{A}:

$\frac{B < : A}{t y p e \{B\} < : t y p e \{A\}}$
If a class B is a subtype (subclass) of a class A, and if the constructor function of B is a subtype of the constructor function of A, then the classifier type constructor{B} also is a subtype of constructor{A} :

$\frac{B < : A B . c t o r < : A . c t o r}{c o n s t r u c t o r \{B\} < : c o n s t r u c t o r \{A\}}$

The subtype relation of the constructor function is defined in Function Type. In the case of the default N4Object constructor, the type of the object literal argument depends on required attributes.

This subtype relation for the constructor type is enforced if the constructor of the super class is marked as final, see Constructor and Classifier Type for details.
The type of a classifier declaration or classifier expression is the constructor of that class:

$\frac{μ (C) \in \{c l a s s i f i e r D e f i n i t i o n\}}{Γ ⊢ C : constructor[C]}$
A class cannot be called as a function in ECMAScript. Thus, the constructor and type type are only subtype of Object:

$\forall T :$
$constructor \{T\} < : Object$
$type \{T\} < : Object$
If the type argument of the constructor is not a declared type (i.e., a wildcard or a type variable with bounds), the constructor cannot be used in a new expression. Thus, the constructor function signature becomes irrelevant for subtype checking. In that case, the following rules apply:

$\begin{matrix} \frac{S . u p p e r < : T . u p p e r T . l o w e r < : S . l o w e r μ (T) \neq DeclaredTypeWithAccessModifier}{constructor S < : constructor T} \end{matrix}$

Note that this is only true for the right hand side of the subtyping rule. A constructor type with a wildcard is never a subtype of a constructor type without a wildcard.

The figure Classifier and Constructor Type Subtype Relations shows the subtype relations defined by the preceding rules.

Figure 4. Classifier and Constructor Type Subtype Relations

Consequences:

Overriding of static methods is possible and by using the constructor or classifier type, polymorphism for static methods is possible as well.

Example 22. Static Polymorphism

class A {
    static foo(): string { return "A"; }
    static bar(): string { return this.foo(); }
}
class B extends A {
    @Override
    static foo(): string { return "B"; }
}

A.bar(); // will return "A"
B.bar(); // will return "B", as foo() is called polymorphical

It is even possible to refer to the constructor of an abstract class. The abstract class itself cannot provide this constructor (it only provides a type..), that is to say only concrete subclasses can provide constructors compatible to the constructor.
Example 23. Constructor of Abstract Class
abstract class A {} class B extends A {} function f(ctor: constructor{A}): A { return new ctor(); } f(A); // not working: type{A} is not a subtype of constructor{A}. f(B); // ok

Allowing wildcards on constructor type references has pragmatic reasons. The usage of constructor references usually indicates very dynamic scenarios. In some of these scenarios, e.g., in case of dynamic creation of objects in the context of generic testing or injectors, arbitrary constructors may be used. Of course, it won’t be possible to check the correct new expression call in these cases – and using new expressions is prevented by N4JS if the constructor reference contains a wildcard. But other constraints, implemented by the client logic, may guarantee correct instantiation via more dynamic constructors, for example via the ECMAScript 2015 reflection API. In order to simplify these scenarios and preventing the use of any, wildcards are supported in constructors. Since a constructor with a wildcard cannot be used in a new expression anyway, using a classifier type is usually better than using a constructor type with wildcard.

Using wildcards on classifier types would have the same meaning as using the upper bound directly. That is, a type reference type{? extends C} can simply be replaced with type{c}, and type{?} with type{any}.

To conclude this chapter, let us compare the different types introduced above depending on whether they are used with wildcards or not:

having a value of type constructor{C}, we know we have
- a constructor function of {C} or a subclass of {C},
- that can be used for instantiation (i.e. the represented class is not abstract),
- that has a signature compatible to the owned or inherited constructor of {C}.
  
  This means we have the constructor function of class {C} (but only if is non-abstract) or the constructor function of any non-abstract subclass of {C} with an override compatible signature to that of {C}'s constructor function.
having a value of type constructor{? extends C}, we know we have
- a constructor function of {C} or a subclass of {C},
- that can be used for instantiation (i.e. the represented class is not abstract).
  
  So, same situation as before except that we know nothing about the constructor function’s signature. However, if {C} has a covariant constructor, cf. Covariant Constructors, we can still conclude that we have an override compatible constructor function to that of {C}, because classes with covariant constructors enforce all their subclasses to have override compatible constructors.
have a value of type type{? extends C} or type{C} (the two types are equivalent), we know we have:
- an object representing a type (often constructor functions are used for this, e.g. in the case of classes, but could also be a plain object, e.g. in the case of interfaces),
- that represents type {C} or a subtype thereof,
- that cannot be used for instantiation (e.g. could be the constructor function of an abstract class, the object representing an interface, etc.).

Slightly simplified, we can say that in the first above case we can always use the value for creating an instance with new, in the second case only if the referenced type has a covariant constructor, cf. Covariant Constructors, and never in the third case.

4.11.3. Constructors and Prototypes in ECMAScript 2015

Constructors and prototypes for two classes A and B in ECMAScript 2015 (not N4JS!) for two classes A and B in ECMAScript 2015 shows the constructors, prototypes, and the relations between them for the ECMAScript 2015 code shown in Constructors and Prototypes.

Example 24. Constructors and Prototypes

class A {}
class B extends A {}

var b = new B();

Constructors and prototypes for two classes A and B in ECMAScript 2015 (not N4JS!) shows plain ECMAScript 2015 only. Also note that A is defined without an extends clause, which is what ECMAScript 2015 calls a base class (as opposed to a derived class). The constructor of a base class always has Function.prototype as its prototype. If we had defined A as class A extends Object {} in the listing above, then the constructor of A would have Object’s constructor as its prototype (depicted in as a dashed red arrow), which would make a more consistent overall picture.

Figure 5. Constructors and prototypes for two classes A and B in ECMAScript 2015 (not N4JS!)

Base classes in the above sense are not available in N4JS. If an N4JS class does not provide an extends clause, it will implicitly inherit from built-in class N4Object, if it provides an extends clause stating Object as its super type, then it corresponds to what is shown in Constructors and prototypes for two classes A and B in ECMAScript 2015 (not N4JS!) with the red dashed arrow.

4.12. This Type

The this keyword may represent either a this literal (cf. This keyword and type in instance and static context) or may refer to the this type. In this section, we describe the latter case.

Typical use cases of the this type include:

declaring the return type of instance methods
declaring the return type of static methods
as formal parameter type of constructors in conjunction with use-site structural typing
the parameter type of a function type expression, which appears as type of a method parameter
the parameter type in a return type expression ( $t y p e$ {this},constructor{this})
an existential type argument inside a return type expression for methods (e.g.ArrayList<? extends this> method(){…})

The precise rule where it may appear is given below in [Req-IDE-37].

The this type is similar to a type variable, and it is bound to the declared or inferred type of the receiver. If it is used as return type, all return statements of the methods must return the this keyword or a variable value implicitly inferred to a this type (e.g. var x = this; return x;).

Simple This Type

class A {
    f(): this {
        return this;
    }
})
class B extends A {}

var a: A; var b: B;
a.f(); // returns something with the type of A
b.f(); // returns something with the type of B

this can be thought of as a type variable which is implicitly substituted with the declaring class (i.e. this type used in a class {A} actually means <? extends A>).

4.12.1. Syntax

ThisTypeRef returns ThisTypeRef:
    ThisTypeRefNominal | ThisTypeRefStructural;

ThisTypeRefNominal returns ThisTypeRefNominal:
    {ThisTypeRefNominal} 'this'
;

ThisTypeRefStructural  returns ThisTypeRefStructural:
        typingStrategy=TypingStrategyUseSiteOperator
        'this'
        ('with' '{' ownedStructuralMembers+=TStructMember* '}')?
;

The keyword this and the type expression this look similar, however they can refer to different types. The type always refers to the type of instances of a class. The this keyword refers to the type of instances of the class in case of instance methods, but to the classifier the of the class in case of static methods. See This Keyword for details.

Example 25. This keyword and type in instance and static context

Note that the following code is not working, because some usages below are not valid in N4JS. This is only to demonstrate the types.

class C {
    instanceMethod() {
        var c: this = this;
    }
    static staticMethod() {
        var C: type{this} = this;
    }
}

Structural typing and additional members in structural referenced types is described in Structural Typing.

4.12.2. Semantics

Req. IDE-37: This Type (ver. 1)

this used in the context of a class is actually inferred to an existential type ? extends A inside the class itself.
the this type may only be used
- as the type of a formal parameter of a constructor, if and only if combined with use-site structural typing.
- at covariant positions within member declarations, except for static members of interfaces.

Remarks

Due to the function subtype relation and constraints on overriding methods (in which the overriding method has to be a subtype of the overridden method), it is not possible to use the this type in formal parameters but only as return type. The following listing demonstrates that problem:
```
class A {
    bar(x: this): void { ... } // error
    // virtually defines: bar(x: A): void
}
class B extends A {
    // virtually defines: bar(x: B): void
}
```
As the $t h i s$ type is replaced similar to a type variable, the virtually defined method bar in is not override compatible with bar in A.

In case of constructors, this problem does not occur because a subclass constructor does not need to be override compatible with the constructor of the super class. Using $t h i s$ as the type of a constructor’s parameter, however, would mean that you can only create an instance of the class if you already have an instance (considering that due to the lack of method overloading a class can have only a single constructor), making creation of the first instance impossible. Therefore, $t h i s$ is also disallowed as the type of a constructor’s parameter.
The difference between the type $t h i s$ and the keyword this is when and how theactual type is set: the actual type of the $t h i s$ type is computed at compile(or validation) time and is always the containing type (of the member in which the type expression is used) or a subtype of that type – this isnot a heuristic, this is so by definition. In contrast, the actual typeof the keyword this is only available at runtime, while the type used at compilation time is only a heuristically-computed type, in other words,a good guess.
The value of the $t h i s$ type is, in fact, not influenced by any @This annotations. Instead of using $t h i s$ in these cases, the type expressions in the @This annotations can be used.
The $t h i s$ type is always bound to the instance-type regardless of the context it occurs in (non-static or static). To refer to the this-classifier (static type) the construct type{this} is used.

Example 26. This type in function-type-expression

class A {
    alive: boolean = true;
    methodA(func: {function(this)}): string {
       func(this);   // applying the passed-in function
       return "done";
    }
}

The use of $t h i s$ type is limited to situations where it cannot be referred in mixed co- and contra-variant ways. In the following example the problem is sketched up. ^[26]

Example 27. Problems with this type and type arguments

// Non-working example, see problem in line 15.
class M<V> {  public value: V;  }
class A {
    public store: M<{function(this)}>; // usually not allowed, but let's assume it would be possible----
}
class B extends A { public x=0; } // type of store is M<{function(B)}>

var funcA = function(a: A) {/*...something with a...*/}
var funcB = function(b: B) { console.log(b.x); }
var a: A = new A();  var b: B = new B();
b.store.value = funcA  // OK, since {function(A)} <: {function(B)}
b.store.value = funcB  // OK.

var a2: A = b; // OK, since B is a subtype of A
a2.store.value( a ) // RUNTIME ERROR, the types are all correct, but remember b.store.value was assigned to funcB, which can only handle subtypes of B!

4.13. Enums

Enums are an ordered set of literals. Although enums are not true classes, they come with built-in methods for accessing value, name and type name of the enum.

In N4JS, two flavours of enumerations are distinguished: ordinary enums (N4JS) and string based enums. Ordinary enums (or in short, enums) are used while programming in N4JS. String based enums are introduced to access enumerations derived from standards, mainly developed by the W3C, in order to access the closed set of string literals defined in webIDL syntax.

4.13.1. Enums (N4JS)

Definition and usage of an enumeration:

// assume this file to be contained in a package "myPackage"
enum Color {
    RED, GREEN, BLUE
}

enum Country {
    DE : "276",
    US : "840",
    TR : "792"
}

var red: Color = Color.RED;
var us: Country = Country.US;

console.log(red.name); // --> RED
console.log(red.value); // --> RED
console.log(red.n4class.fqn); // --> myPackage.Color
console.log(red.toString()); // --> RED

console.log(us.name); // --> US
console.log(us.value); // --> 840
console.log(us.n4classfqn); // --> myPackage.Country
console.log(us.toString()); // --> 840

4.13.1.1. Syntax

N4EnumDeclaration <Yield>:
	=>(	{N4EnumDeclaration}
		(declaredModifiers+=N4Modifier)*
		'enum' name=BindingIdentifier<Yield>? )
	'{'
		(literals+=N4EnumLiteral (',' literals+=N4EnumLiteral)*)?
	'}';

N4EnumLiteral: name=IdentifierName (':' value=STRING)?;

4.13.1.2. Semantics

The enum declaration $E$ is of type type{E} and every enumeration is implicitly derived from N4Enum. There are similarities to other languages such as Java, for example, where the literals of an enum are treated as final static fields with the type of the enumeration and the concrete enumeration provides specific static methods including the literals. This leads to the following typing rules:

Req. IDE-38: Enum Type Rules (ver. 1)

For a given enumeration declaration $E$ with literals $L$ , the following type rules are defined:

Every enumeration $E$ is a subtype of the base type N4Enum:

$\frac{}{Γ ⊢ E < : N 4 E n u m}$

which itself is a subtype of Object:

$\frac{}{N 4 E n u m < : O b j e c t}$
Every literal $L$ of an enumeration $E$ is of the type of the enumeration:

$\frac{L \in E . l i t e r a l s}{Γ ⊢ L : E}$

This means that every literal is a subtype of N4Enum and Object:

\frac{L \in E . l i t e r a l s}{L < : N 4 E n u m \land L < : O b j e c t}

The base enumeration type N4Enum is defined as follows:

/**
 * Base class for all enumeration, literals are assumed to be static constant fields of concrete subclasses.
 */
public object N4Enum {

    /**
     * Returns the name of a concrete literal
     */
    public get name(): string

    /**
     * Returns the value of a concrete literal. If no value is
     * explicitly set, it is similar to the name.
     */
    public get value(): string

    /**
     * Returns a string representation of a concrete literal, it returns
     * the same result as value()
     */
     public toString(): string

    /**
     * Returns the meta class object of this enum literal for reflection.
     * The very same meta class object can be retrieved from the enumeration type directly.
     */
    public static get n4type(): N4EnumType

    //IDE-785 this as return type in static

    /**
     * Returns array of concrete enum literals
     */
    public static get literals(): Array<? extends this>

    /**
     * Returns concrete enum literal that matches provided name,
     * if no match found returns undefined.
     */
    public static findLiteralByName(name: string): this

    /**
     * Returns concrete enum literal that matches provided value,
     * if no match found returns undefined.
     */
    public static findLiteralByValue (value: string): this
}

Req. IDE-39: Unique literal names (ver. 1)

$\forall i, j : l i t e r a l s [i] . n a m e = l i t e r a l s [j] . n a m e \Leftrightarrow i = j$

Literal names have to be unique.

Req. IDE-40: Enum Literals are Singletons (ver. 1)

Enum literals are singletons:

\forall e_{1}, e_{2}, μ (e_{1}) = μ (e_{2}) = N4EnumLiteral \land Γ ⊢ e_{1} = Γ ⊢ e_{2} : e_{1} = = e_{2} \Leftrightarrow e_{1} = = = e_{2}

Example 28. Enumeration List

Due to the common base type N4Enum it is possible to define generics accepting only enumeration, as shown in this example:

enum Color { R, G, B}

class EList<T extends N4Enum> {
    add(t: T) {}
    get(): T { return null; }
}

var colors: EList<Color>;
colors.add(Color.R);
var c: Color = colors.get();

4.13.2. String-Based Enums

In current web standards [W3C:Steen:14:XL], definitions of enumerations are often given in webIDL syntax. While the webIDL-definition assembles a set of unique string literals as a named enum-entity, the language binding to ECMAScript refers to the usage of the members of these enumerations only. Hence, if an element of an enumeration is stored in a variable or field, passed as a parameter into a method or function or given back as a result, the actual type in JavaScript will be string. To provide the N4JS user with some validations regarding the validity of a statement at compile time, a special kind of subtypes of string are introduced: the string-based enum using the @StringBased annotation. (See also other string-based types like typename<T> pathSelector<T> and i18nKey in Primitive Pathselector and I18nKey.)

String-based enums do not have any kind of runtime representation; instead, the transpiler will replace each reference to a literal of a string-based enum by a corresponding string literal in the output code. Furthermore, no meta-information is available for string-based enums, i.e. the n4type property is not available. The only exception is the static getter literals: it is available also for string-based enums and has the same meaning. In case of string-based enums, however, there won’t be a getter used at runtime; instead, the transpiler replaces every read access to this getter by an array literal containing a string literal for each of the enum’s literals.

Req. IDE-41: String-Based Enum Type Rules (ver. 1)

For a string-based enum declaration $E_{S}$ with literals $L_{S}$ the following type rules are defined:

Every string-based enumeration $E_{S}$ is a subtype of the base type N4StringBasedEnum:

$\frac{}{Γ ⊢ type \{E_{S}\} < : N4StringBasedEnum}$

which itself is not related to the standard enumeration type N4Enum

$\begin{matrix} \frac{}{N4StringBasedEnum ≮ : N4Enum} \\ \frac{}{N4Enum ≮ : N4StringBasedEnum} \end{matrix}$
N4StringBasedEnum is a subtype of string

$\begin{matrix} \frac{}{N4StringBasedEnum < : string} \end{matrix}$
Each literal in $L_{S}$ of a string-based enumeration $E_{S}$ is of the type of the string-based enumeration.

$\frac{l \in E_{S} . L_{S}}{Γ ⊢ l < : E_{S}}$
[Req-IDE-39] also applies for N4StringBasedEnum.
[Req-IDE-40] also applies for N4StringBasedEnum.
References to string-based enums may only be used in the following places:
1. in type annotations
2. in property access expressions to refer to one of the enum’s literals
3. in property access expressions to read from the static getter literals
  
  In particular, it is invalid to use the type of a string-based enum as a value, as in
  @StringBased enum Color { RED, GREEN, BLUE } var c = Color;

Example 29. WebIDL example

Gecko-Engine webIDL XMLHttpRequestResponseType as taken from [W3C:Steen:14:XL]

enum XMLHttpRequestResponseType {
  "",
  "arraybuffer",
  "blob",
  "document",
  "json",
  "text" //, ... and some mozilla-specific additions
}

Compatible Definition of this Enumeration in N4JS, provided through a runtime-library definition:

File in source-folder: w3c/dom/XMLHttpRequestResponseType.n4js

@StringBased enum XMLHttpRequestResponseType {
  vacant : "",
  arrayBuffer : "arraybuffer",
  blob : "blob",
  document : "document",
  json : "json",
  text : "text"
 }

Usage of the enumeration in the definition files of the runtime-library. Note the explicit import of the enumeration.

XMLHttpRequestResponse.n4jsd

@@ProvidedByRuntime
import XMLHttpRequestResponseType from "w3c/dom/XMLHttpRequestResponseType";
@Global
export external public class XMLHttpRequestResponse extends XMLHttpRequestEventTarget {
  // ...
  // Setter Throws TypeError Exception
  public responseType: XMLHttpRequestResponseType;
  // ...
}

Client code importing the runtime-library as defined above can now use the Enumeration in a type-safe way:

String-Based Enumeration Usage

import XMLHttpRequestResponseType from "w3c/dom/XMLHttpRequestResponseType";

public function process(req: XMLHttpRequest) : void {
  if( req.responseType == XMLHttpRequestResponseType.text ) {
    // do stuff ...
  } else {
       // signal unrecognized type.
       var errMessage: req.responseType + " is not supported"; // concatination of two strings.
       show( errMessage );
  }
}

4.14. Short-Hand Syntax

Short-hand syntax is available for a number of built-in types.

4.14.1. Array Short-Hand Syntax

For the built-in type Array a convenience short form is available. Thus, writing

let arr: string[];

is equivalent to

let arr: Array<string>;

Multi-dimensional arrays can be declared as such:

let arr: string[][][];

which is equivalent to

let arr: Array<Array<Array<string>>>;

4.14.2. IterableN Short-Hand Syntax

The built-in IterableN types (i.e. Iterable2, Iterable3, … Iterable9, see IterableN) are also provided with a short-hand syntax. For example, writing

let i3: [string,number,string[]];

would be equivalent to

let i3: Iterable3<string,number,Array<string>>;

Note the following special cases:

let i0: [];
let i1: [string];
let union: string|number[];

which is equivalent to

let i0: Iterable<?>;
let i1: Iterable<string>;
let union: union{string,Array<number>}; // not: Array<union{string,number}>

Further note: while this syntax is very similar to TypeScript’s tuple syntax, the semantics of tuples and IterableN are very different.

N4JS Language Specification

ECMAScript Types

N4Types

Syntax

Properties

Semantics

Type Inference

Syntax

Properties

Semantics

Type Inference

Semantics

Semantics

Semantics

Semantics

Quick Links