Type Checking

PPL 2023

This lecture introduces type checking and type inference with illustration in TypeScript.

Why Types

Adding types to a program has three key advantages:

Adding types is sometimes “annoying” because it can make programs longer, and for complicated types or generic types - it can make simple programs complex. For example, a function such as x => x (known as the identity function) has a complex type (because it can work on any possible types). We will see further examples of this later.

TypeScript alleviates these 2 problems by:

This approach is called gradual typing. As a general strategy in programming languages, gradual typing allows programmers to trade-off prototyping and type safety.

Runtime Errors Caused by Unexpected Values

Consider the following type definition and the function operating over values in this type:

import { map } from "ramda";

type Date = {
	year: number;
	month: number;
	day: number;
}

type Person = {
	birthDate: Date;
	name: string;
}

const computeAges = (persons) => map(p => 2023 - p.birthDate.year, persons);

let persons = [
	{ name: "avi", birthDate: { year: 1992, month: 7, day: 10 } },
	{ name: "batia", birthDate: { year: 1996, month: 3, day: 2 } }
];

console.log(computeAges(persons)); // ==> [ 31, 27 ]

Consider now what happens if we invoke computeAges on this value:

computeAges([{ name: "avi" }, { name: "batia" }]);
// ==> Uncaught TypeError: Cannot read properties of undefined (reading 'year')

We obtain a runtime error when we try to access a property of a map which is not provided in the actual value passed to the function.
In other words, there is an incompatibility between the value passed to the function and the type of the value expected by the function.

Type annotations are introduced in programming languages to enable type checking. Type checking is a process that analyzes a program and verifies that such incompatibities between variables or function parameters and the values to which they are bound at runtime are impossible for all possible executions of the program.

When type checking is performed at compilation, it detects errors that could otherwise occur later at runtime. This is a much better situation - errors caught early are errors that are avoided. Errors caught at runtime cause damage.

Compilers that implement type checking provide an extremely powerful form of program verification. If we change our function declaration as follows, with a type declaration for the parameter of the function computeAges as persons: Person[], the compiler can verify that the invocation of the function can lead to a runtime type error, and apparently it is not the behavior intended by the programmer. In this case, compilation fails and a helpful compilation error message is provided.

import { map } from "ramda";

type Date = {
	year: number;
	month: number;
	day: number;
}

type Person = {
	birthDate: Date;
	name: string;
}

const computeAges = (persons: Person[]) => map(p => 2023 - p.birthDate.year, persons);

let persons = [
	{ name: "avi", birthDate: { year: 1992, month: 7, day: 10 } },
	{ name: "batia", birthDate: { year: 1996, month: 3, day: 2 } }
];

console.log(computeAges(persons)); // ==> [ 31, 27 ]
computeAges([{ name: "avi" }, { name: "batia" }]);
// --> Compile error: Property birthDate is missing in type {name: string} but required in type Person.

Why Would Anyone Give Up on Type Checking?

Given that type checking is such a powerful tool - why would any programmer want to give up this and use a programming language that does not provide it?

The arguments usually advanced by proponents of languages without type checking are the following:

There are other arguments in favor of untyped languages which we will not develop further that are related to the type of polymorphism that is encouraged by each style. In this course, we strongly adopt the typed style of programming (we have chosen our camp :-) ).

Types in TypeScript

TypeScript adds optional type declarations to JavaScript.

The principles of this addition are:

// The following TypeScript expression
let add: (a: number, b: number) => number = (a, b) => a + b;
add(1, 2);

// is translated by tsc into:
let add = (a, b) => a + b;
add(1, 2);

Type Annotations

Type annotations are optional in TypeScript. They can occur in the following contexts:

// After variable declarations
let varName: <typeAnnotation>;  

// As part of a function signature
(param: <typeAnnotation>, ...) => ...

function fname(param : <typeAnnotation>, ...): <typeAnnotation> { ... }

Type annotation are written in a specific form - which is called the type language. The type language is used to describe the expected type of variables, parameters or the value returned by functions.

Type Expression Denotation

In general, all type expressions in the type language are used to refer to a specific set of values. The relation between a type expression and a set of values to which it corresponds is called denotation. (The denotation relation is in general the relation that exists between a name and the object to which the name refers.)

Atomic Type Expressions

The simplest type language expression refers to a primitive type - for example number, boolean, string.

It is used as follows:

let x: number = 2;
let a: string = "a";
let b: boolean = true;
b; // ==> true

These atomic type expressions denote the primitive sets of values that are defined in JavaScript (set of all number values, set of all string values, set of a boolean values).

More complex type language expressions are needed to describe types over compound values. These compound type expressions are constructed recursively by combining smaller type expressions

Array Type Expressions

To describe a homogeneous array, the following notation is used: <typeAnnotation>[]

let stringArr: string[] = ["a", "b", "c"];
let s: string = stringArr[0];
s; // ==> 'a'

The following values are not compatible with this type annotation:

stringArr = ['a', 1]  // Item 1 has wrong type
stringArr[0] = true;  // Item 0 has wrong type

Map Type Expressions

To describe map types, the following notation is used:

{ <key>: <typeAnnotation>; ... }

let s: { name: string; cs: boolean; age: number } = {
    name: "avi",
    gender: "m",
    cs: true,
    age: 22
};
s; // ==> { name: 'avi', gender: 'm', cs: true, age: 22 }

The expected meaning of the map type description is that all the keys in the annotation must be present in the value with the described type.

There could be more keys as illustrated in the assignment s = s2 below - but all the keys that are specified in the type must be present.

Note, however, that when we bind a variable to a literal expression, the TypeScript compiler demands that the type of the literal be exactly that of the variable - with no extension.

let s: { name: string; cs: boolean; age: number } = {
    name: "avi",
    cs: true,
    age: 22
};
s = { age: 22, name: "avi", cs: true }; // OK - The order of keys is not important
s = { name: "avi", age: 22 }; // Error: missing key "cs"
s = { name: "avi", age: "22", cs: true }; // Error: key "age" must be a string
s = { name: "avi", age: 22, cs: true, gender: "m" }; // NOT OK for a literal because of additional key "gender"
let s2: { name: string; cs: boolean; age: number; gender: string } = {
    name: "avi",
    age: 22,
    cs: true,
    gender: "m"
};
s = s2; // OK even though s2 has more properties - it satisfies the requirements of s's type.
s; // ==> { name: 'avi', age: 22, cs: true, gender: 'm' }

Map Types Relationships

The map type {} denotes all possible map values.

The map type { a: string } denotes all maps that have a key a with a string value - for example:

{ a: "x" }
{ a: "y", b: 1 }

and the following values are not part of this type:

{}
{ b: 1 }
{ a: 1 }

A map type { a: string, b: number } denotes all maps that have a key a with a string value and a key b with a number value.

We infer from this definition that the type { a: string, b: number } is a strict sub-type of the type { a: string }.

What is the relation between the types?

type mapAB = { a: string, b: number };
type mapAC = { a: string, c: boolean };

These two types are distinct:

{ a: "x", b: 2 } is in mapAB and not in mapAC. { a: "x", c: true } is in mapAC and not in mapAB.

Yet - they have a non-empty overlap:

{ a: "x", b: 2, c: true } is both in mapAB and in mapAC.

In general - the intersection of the types mapAB and mapAC is the type:

type mapABC = { a: string, b: number, c: boolean };

The following types are disjoints:

type mapAS = { a: string };
type mapAN = { a: number };

because the constraints on the value of the key a are incompatible.

A good way to think about these relations is the following:

Named Type Expressions

Type expressions can be given names. For example, a map type expression can be named using the type alias construct:

type <typeName> = {
    <key>: <typeAnnotation>;
    ...
}

type Student = {
    name: string;
    cs: boolean;
    age: number;
}

let s: Student = { name: "avi", cs: true, age: 22 };
type stringArray = string[];
s; // ==> { name: 'avi', cs: true, age: 22 }

Embedded Type Expressions

A type expression can have arbitrary type expressions embedded recursively. For example:

type Course = {
    courseName: string;
    dept: string;
    semester: number;
    year: number;
};

type RegisteredStudent = {
    name: string;
    cs: boolean;
    age: number;
    courses: Course[];
};

// This is a valid JSON value for the RegisteredStudent type
let rs: RegisteredStudent = {
    name: "avi",
    cs: true,
    age: 12,
    courses: [{ courseName: "ppl", dept: "cs", semester: 2, year: 2021 }]
};

// This is NOT a valid JSON value for the RegisteredStudent type:
let badRs: RegisteredStudent = {
    name: "avi",
    cs: true,
    age: 12,
    courses: [{ courseName: "ppl", dept: "cs", year: 2021 }] // badRs.courses[0] is missing key semester.
};

rs;
// ==>
// {
//     name: "avi",
//     cs: true,
//     age: 12,
//     courses: [{ courseName: "ppl", dept: "cs", semester: 2, year: 2021 }]
// }

The TypeScript compiler (tsc) emits this error:

Property 'semester' is missing in type '{ courseName: string; dept: string; year: number; }' but required in type 'Course'.

Implicit Type Annotations

TypeScript can infer the type of variables based on their usage. This is called an implicit type annotation. For example:

let a = 1;
a = 'nok'; // type error

On the assignment line a = 'nok', tsc emits this error:

Type 'string' is not assignable to type 'number'.

This means that tsc detected that the variable a is of type number based on its bound value 1. From this point on, it checks that a keeps a number value.

Type Queries

One can use the following notation to declare that a variable should have the type of another variable:

let p1 = { name: "avi", age: 22 };
let p2: typeof p1 = { name: "nok" };

In this case, tsc emits this error:

Property 'age' is missing in type '{ name: string; }' but required in type '{ name: string; age: number; }'.

TypeScript detects that the type of p1 is { name: string, age: number; } on the basis of the value of p1 - even though the type of p1 was not declared - it was inferred from its value.

The typeof var construct is called a type query in TypeScript.

NOTE:

The typeof p1 type query annotation is different from the typeof operator we discussed in the previous lecture - which is a primitive runtime operator in JavaScript.

The TypeScript typeof is a type annotation - it belongs to the Type Language - its value is a type annotation.

The JavaScript typeof is a runtime primitive operator. Its value is a string.

// JavaScript typeof
const p3 = 2;
typeof p3; // ==> 'number'

Recursive Types

Consider the case of defining a binary tree. Using JSON, we would encode a binary tree as follows:

let binTree = {
    root: 1,
    left: { root: 2 },
    right: { root: 3 }
};
binTree; // ==> { root: 1, left: { root: 2 }, right: { root: 3 } }

The TypeScript type that corresponds to this value would be:

{
    root: number;
    left: ?;
    right: ?;
}

We would need to specify that the left and right keys expect to receive values of exactly the same type. The only way to achieve such a declaration is to use a recursive type declaration – which requires us to give a name to the type:

type BinTree = {
    root: number;
    left: BinTree;
    right: BinTree;
}

Let us try to create a value according to this type specification:

type BinTree = {
    root: number;
    left: BinTree;
    right: BinTree;
}

let bn: BinTree = {
    // DOES NOT PASS TYPE CHECKING
    root: 1,
    left: { root: 2 },
    right: { root: 3 }
};

Unfortunately, this value is not well typed - tsc returns this error:

Type '{ root: number; }' is missing the following properties from type 'BinTree': left, right

That is - we are missing the keys left and right for the nodes with root 2 and 3. In other words, we cannot stop the recursion - the value must keep unrolling to be a valid BinTree.

There are multiple solutions to this problem. One is to indicate that the properties left and right are optional. This is indicated using the ? syntax as follows:

type BinTree = {
    root: number;
    left?: BinTree;
    right?: BinTree;
}

let bn: BinTree = {
    root: 1,
    left: { root: 2 },
    right: { root: 3, right: { root: 4 } }
};

bn;
// ==>
// { root: 1,
//   left: { root: 2 },
//   right: { root: 3, right: { root: 4 } } }

Other solutions rely on type unions which we will review later in the course.

NOTE:

How different is the type annotation: { a?: string, b: number } from: { a: any, b: number }?

Answer: the difference is that a: any means that the property a can have any possible value; in contrast a?: string means that either a does not occur at all or if it occurs it must have a value of type string.

Generic Types

If we want to define a binary tree whose nodes can have any type - but where all the nodes in the tree must have the same type, we must introduce type variables.

type BinTree<T> = {
    root: T;
    left?: BinTree<T>;
    right?: BinTree<T>;
}

let bn: BinTree<number> = {
    root: 1,
    left: { root: 2 },
    right: { root: 3 }
};

bn; // ==> { root: 1, left: { root: 2 }, right: { root: 3 } }

If we want to use a heterogeneous tree (a tree that can contain nodes of different types), we can use the special type called any:

let an: BinTree<any> = {
    root: "different",
    left: { root: 1, left: { root: false } }
};

an; // ==> { root: 'different', left: { root: 1, left: { root: false } } }

The any type is compatible with all values - it denotes the set of all possible values. Every type that can be defined is actually a subset of the any type. In itself, any is not useful - typing a variable as any does not indicate any constraint on the variable. But when used as a type parameter in a complex type definition as above, any becomes useful.

When Are Generic Types Useful?

Generic types are compound type expressions with type variables. Some of their components are thus left as unspecified types. When are such partially unspecified types useful?

const treeNodesNumber: <T>(t: BinTree<T>) => number = t => {
    if (t === undefined) return 0;
    else return 1 + treeNodesNumber(t.left) + treeNodesNumber(t.right);
};
treeNodesNumber({ root: 1, left: { root: 2 }, right: { root: 3 } }); // ==> 3

const treeDepth: <T>(t: BinTree<T>) => number = t => {
    if (t === undefined) return 0;
    else return 1 + Math.max(treeDepth(t.left), treeDepth(t.right));
};

treeDepth({
    root: 1,
    left: { root: 2, left: { root: 4 } },
    right: { root: 3 }
}); // ==> 3

We can define it as generic type as follows:

type ArrayMin<T> = {
    min: T;
    values: T[];
}

let numberArrayMin: ArrayMin<number> = {
    min: 2,
    values: [6, 2, 4]
};

let stringArrayMin: ArrayMin<string> = {
    min: "avi",
    values: ["bibi", "charles", "avi"]
};

stringArrayMin.min; // ==> 'avi'

The relation between the two components of these values is the same - regardless of the actual type (number, string) of the components.

Naturally, the two motivations for using generic types combine well together - generic algorithms work well over dependent components.

Generic Types Relationships

What is the type relationship (inclusion, disjointness) between BinTree<T> and BinTree<number>?

We first need to realize that the type expression BinTree<T> cannot be used as the type of a variable if it is not in the scope of a type variable. That is, the expression:

let b : BinTree<T> = ...;

is not possible - because BinTree<T> cannot be in itself the type of a variable.
A generic type can only appear in the context of a generic function (like in the example treeDepth and treeNodesNumber above) or in the context of a larger generic type.

When the tree variable is instantiated to a concrete (non-generic) type, then the type can be used as any other type:

let st : BinTree<string> = { root: "avi", left: { root: "bibi" } };

The relation between a generic type such as BinTree<T> and a type such as BinTree<string> is called instantiation.

Now, what is the relation between BinTree<string> and BinTree<number>? These two concrete types are instances of the same generic type. Any value in BinTree<string> has a property root of type string. Any value in BinTree<number> has a property root of type number. We infer that these two types are disjoint.

Note that while these two types are disjoint, we still can write generic functions that operate of values of either type using the same code.

If a type S is a subtype of a type T, then what is the relation between the types BinTree<S> and BinTree<T>? For example, consider T = { name: string } and S = { name: string, age: number }.

To answer this question, we can read the definition of BinTree<T> as a set of constraints a value must meet to belong to the type this type expression denotes:

Knowing that any value of type S is also a value of type T (by definition of subtyping), we can infer that any value in BinTree<S> meets all the constraints to also belong to BinTree<T>.

In general, if S is a subtype of T, then BinTree<S> is a subtype of BinTree<T>.

Function Types

One can type functions in TypeScript. Let us introduce function types step by step:

An untyped function in JavaScript has the following form:

// Named function
function add(x, y) {
    return x + y;
}

// Anonymous function
const myAdd = function (x, y) {
    return x + y;
};

// Using the fat arrow notation:
const myFatAdd = (x, y) => x + y;

console.log(myFatAdd(2, 3)); // ==> 5

We can first specify the types of the parameters and the return type, in a way similar to the way it would be done in Java. This applies both to named functions and to anonymous functions.

// Named function
function add(x: number, y: number): number {
    return x + y;
}

// Anonymous function
const myAdd = function (x: number, y: number): number {
    return x + y;
};

// Using the fat arrow notation:
const myFatAdd = (x: number, y: number): number => x + y;

console.log(myFatAdd(2, 3)); // ==> 5

Let us now write the full type of the function out of the function value:

let myAdd: (x: number, y: number) => number = function (x, y) {
    return x + y;
};

let myFatAdd: (x: number, y: number) => number = (x, y) => x + y;

console.log(myFatAdd(3, 4)); // ==> 7

The type expression:

(x: number, y: number) => number

is a function type. The values that this type denotes are functions that map a pair of numbers to a number - in other words, functions whose domain is within \(Number \times Number\) and whose range is within \(Number\). (Remember that types denote a set of values.)

This notation is called the function signature - it combines the information on the type of the parameters, their name and the type of the returned value.

Parameter names are just to help with readability. We could have instead written:

let myAdd: (baseValue: number, increment: number) => number = function (x: number, y: number): number {
    return x + y;
};

As long as the parameter types align, it’s considered a valid type for the function, regardless of the names you give the parameters in the function type.

The second part of the function type is the return type. We make it clear which is the return type by using a fat arrow (=>) between the parameters and the return type. This is a required part of the function type, so if the function doesn’t return a value (which means this is a function that just has a side-effect - no return value), we use the special type void instead of leaving it off.

Closures and their Type

Consider the following function definition:

let z = 10;
let add: (x: number, y: number) => number = (x, y) => x + y + z;
add(1, 2); // ==> 13

The definition of add refers to the variable z, which is defined outside the body of the function. When this happens, we say that the function captures the variable z - and the value of the function add is called a closure. This is because the function closes the captured variables together with the function definition.

The body of the function depends on the variable z - yet, the signature of the function does not indicate this dependency.

Consider the following example that indicates why this capture mechanism is part of the definition of the closure:

let adder = function (inc) {
    return x => x + inc;
};

let a5 = adder(5);
let a2 = adder(2);

console.log(a5(10)); // ==> 15
console.log(a2(10)); // ==> 12
adder(10)(3); // ==> 13

Let us analyze the defintion of the function adder - and refactor it step by step using types.

adder is a function that accepts one parameter inc. What should be the type of inc?

We look at where inc is used in the body of the function adder and find the expression x + inc. This expression appies to numbers - we conclude that z should be a number.

The signature of the function adder should therefore look like:

(inc: number) => ?

What is the type of the value returned by adder?

We analyze the body of adder to identify the returned expression:

function (inc) {
    return x => x + inc;
}

The returned value is x => x + inc. This expression is a function - which receives x as a parameter and return x + inc as a parameter.

The type of this returned function is thus:

(x: number) => number

Putting parameter and return value together, we obtain the type of the function adder as this expression:

(inc: number) => ((x: number) => number)

And adding all the types in the definition of adder we obtain:

let adder: (inc: number) => (x: number) => number = function (inc: number) {
    return (x: number): number => x + inc;
};

Now consider the capturing of the parameter z when the function adder is invoked - in the expression:

let add5 = adder(5);

The type of add5 is (x: number) => number. adder(5) returns a function of one parameter. When it is invoked, this function adds 5 to its parameter.

How does it know to add 5 specifically?

This is because when the return function is computed, it captures the current value of the parameter inc. This happens in the computation of this expression:

Compute adder(5)
Step 1: Bind parameter inc to 5
Step 2: Compute the value (x => x + inc) // This is when variable inc is captured

The key point is that when the value of the function is computed, inc is bound to the value 5. Later, when the value add5 is used, inc is not bound anymore to any value - because the scope of its definition has been exited.

let add5 = adder(5);
console.log(add5(2)); // add5 uses the value of inc which was captured when the closure was created
// ==> 7
console.log(inc); // We confirm that inc is undefined
// ==> Uncaught ReferenceError: inc is not defined

Type of Closures

If we look back at the type of the closures returned when we compute adder(5) - we obtain:

(x: number) => number

In words - it means that the value of adder(5) is a function which receives a number x and returns a number.

Note that the closure does not indicate that it depends on another variable (inc) - because this is not part of the signature of the closure - it is an internal aspect of the closure.

Type Compatibility

As part of the type checking performed by the TypeScript compiler, one must determine whether two type expressions are compatible. This compatibility checking occurs in the following context for example:

Type Compatibility is NOT Symmetric: Subtyping

Type compatibility is not symmetric - T1 is compatible with T2 means we can substitute a value of type T2 with a value of type T1 and still obtain valid expressions. The reverse may not be true.

In general, think of type expressions as expressing constraints on the values that belong to the type. When a type expression T1 expresses more constraints than T2, then it means the type expression T1 denotes less values than T2. It also means all the values in T1 meet the constraints specified by T2.

To remember this - we say that T1 is a subtype of T2 - all the values in T1 satisfy the constraints of T2. When this is the case, it is safe to replace variables of type T2 with values or variables of type T1 - in short, it is safe to perform let t2 = t1.

To remember the rule - remember: let t = s is possible when s < t - meaning we can bind with let (or pass as a parameter) a value or variable of type s to a variable of type t when s is a subtype of t. In this short form, s stands for source, t for target.

Compatibility Rules

We will revisit the rules of type compatibility in Chapter 3.

For now, consider the following practical aspects of type compatibility in TypeScript:

The rules for maps and functions are a bit more complex:

Map Type Compatibility: Structural Typing

Reference: https://www.typescriptlang.org/docs/handbook/type-compatibility.html

The basic rule of TypeScript for Map compatibility is: x is compatible with y if y has at least the same members as x.

For example:

type Named = {
    name: string;
}

let x: Named;

// y's inferred type is { name: string; location: string; }
let y = { name: "Alice", location: "Seattle" };

x = y;

The type expression inferred for y is { name: string, location: string }. It has more constraints than Named.

In TypeScript, these two types are compatible - that is the type of y is a subtype of the Named type.

To check whether y is compatible with the type of x, the compiler checks each property of x to find a corresponding compatible property in y. In this case, y must have a member called name that is a string. It does, so the assignment is allowed.

The same rule for checking the compatibility of the assignment is used when checking function call arguments:

function greet(n: Named) {
    console.log("Hello, " + n.name);
}
greet(y); // OK

Note that y has an extra location property, but this does not create an error. Only members of the target type (Named in this case) are considered when checking for compatibility.

This comparison process proceeds recursively, exploring the type of each member and sub-member.

This method of checking type compatibility is called structural typing. Structural typing is a way of relating types based solely on their members. This is in contrast with nominal typing which we know from Java and C++.

Consider the following code:

type Named = {
    name: string;
}

type Person = {
    name: string;
    age: number;
}

Under structural typing, Person is a subtype of Named - even though this is not declared by the programmer; this subtyping relation is inferred by the compiler.

function greeter(n: Named): string {
    return "Hello " + n.name;
}

let p: Person = { name: "John", age: 26 };
greeter(p); // OK because of structural typing: p declared as a subtype (Person) of Named

In nominally-typed languages like Java, the equivalent code would be an error because the Person type does not explicitly describe itself as being a subtype or an implementor of the Named type - the programmer does not define explicitly relations between the types.

Function Types Compatibility: Comparing the Types of Functions

(This is taken from https://www.typescriptlang.org/docs/handbook/type-compatibility.html):

While comparing primitive types and object types is relatively straightforward, the question of what kinds of functions should be considered compatible is a bit more involved. Let’s start with a basic example of two functions that differ only in their parameter lists:

let x = (a: number, t: string) => 0;
let y = (b: number, s: string) => 0;

y = x; // OK

Comparing Parameters Types

To check if x is assignable to y, we first look at the parameter list. Each parameter in x must have a corresponding parameter in y with a compatible type. Note that the names of the parameters are not considered, only their types. In this case, every parameter of x has a corresponding parameter with identical type in y, so the assignment is allowed.

We ignore here the complexity introduced by optional arguments and differing number of arguments - we will simplify by stating that two function parameter lists are compatible if they have the same length. The comparison of the type of each parameter, however, is surprising.

Comparing Return Types

Let’s look at how return types are treated, using two functions that differ only by their return type:

let x = () => ({ name: "Alice" });
let y = () => ({ name: "Alice", location: "Seattle" });

x = y; // OK
y = x; // Error because x() lacks a location property

The type system enforces that: the source function’s return type be a subtype of the target type’s return type. t = s s.r < t.r

That is - when checking f1: (x: T1) => U1 with f2: (x: T2) => U2 - f1 is a subtype of f2 (meaning f2 = f1 is ok) we verify that U1 is a subtype of U2, but we check the reverse relation for the parameters, that is, T2 is a subtype of T1.

The behavior of parameters and return values for function types when considering subtypes is well explained (with examples) in this post: https://www.stephanboyer.com/post/132/what-are-covariance-and-contravariance.

In short, we say that function (as a type constructor) is contra-variant on parameters and covariant on return type.

Summary

Types

Type Language

Function Types

Type Compatibility