Type Derivation Rules

Why do most typed languages require explicit type annotations?

In C, type annotations help allocate enough memory.

In Java, methods require type annotations for input parameters and return values.

How does a compiler check for well-typedness?

Ensures programs never consume data of the wrong type.

Checks operators that consume data.

Performs checks on the abstract syntax tree (AST)

How does type checking work in an AST?

The compiler traverses the AST to check if operators consume correct data types.

What happens if an expression mixes types incorrectly?

It results in a type error, making the program ill-typed.

What happens when a conditional's result is undecidable?

Example: if (if (0 < 1) then 0 else true) then 0 else (y + 1).

The subtree could be ℕ or 𝔹, making it impossible to determine statically.

This is a problem in statically-typed languages but may not be in dynamically-typed ones

What is needed to check if an AST is well-typed?

Every subtree must have a type (T).

A typing relation ⊢ e : τ must be defined, meaning "expression e has type τ".

Type-checking must be performed locally on syntax trees.

How does a typing relation work?

Defined using derivation rules.

Ensures that if premises (above the line) hold, then the conclusion (below the line) must hold.

What is an inductive set?

A set defined by rules such as:

Base cases:

{a, b} are in S.

Inductive rules:

If α is in S, then αc is in S.If αc is in S, then αcd is in S.

How do inductive sets relate to type derivations?

Programs are inductively defined using their syntax.

Typing rules can be applied one operator at a time.