Types & Type System

Type: What?

(Lol see what I did there?)

Anyways, a type is a classification of data that says:

• What values it can hold (integers, booleans etc)
• The operations that can be performed on it. (concatenation, arithmetic etc)
• The memory layout and how it’s stored on the system.

What’re Type Systems:

A set of rules that governs how types are assigned to variables, functions and expressions. Ideally, the goals are:

• Correctness (e.g. preventing adding a string to an integer - detecting semantic errors).
• Optimisation
• Safety (preventing Buffer Overflow Attack)

Where:

• We operate on the AST

Types of Types (Types${}^2$)

• Statically Typed: We check the types at compile time (C, Java, etc.) - Check before executing the program.

• Dynamically Typed: We the types at runtime (Python)

• Weak Type: Allows implicit type conversions (JS - "10" + 5 = "105").

• Strong Type: Strictly enforces type rules (Python)

• Subtyping: When a variable A is a subtype of variable B, then A can be used anywhere B is expected.

Typing Rule:

It defines how types are assigned to expressions, variables and functions. We denote it with your assumptions at the top and the conclusion at the bottom.

For example:
$\frac{x:T\in \Gamma }{\Gamma ,R⊢x:T}$
Simply: If $x$ is declared in the environment $\Gamma$ with type $T$, then $x$ can be used with type $T$, with return type R.

• The $⊢$ means entrails
• The environment $\Gamma$ stores the type information for variables in scope at a given time.

Environment:

When talking about the environment, we use the following notation:
$O(f)=\{T_1\times \cdots \times T_n\to T_o;x_1,\dots ,x_n;v_1:T_1^{\prime },\dots ,v_m:T_m^{\prime }\}$
Where:

• $O(f)=T$ indicates that variable $f$ is in the local environment and has type $T$
• $T_1,...,T_n$ are the types of the function parameters
• $T_0$ is the return type.
• $x_1,...,x_n$ are the names of the function parameters
• $v_1:T_1^{\prime }$ are the identifiers and types.

Type Checking:

Imagine someone asked you to check the following type:
$O,R⊢\text{False and (True and False)}:\text{bool}$
And you’re only given these 3 rules:
$\frac{}{O,R⊢\text{False}:\text{bool}}\text{[BOOL-FALSE]}$

$\frac{}{O,R⊢\text{True}:\text{bool}}\text{[BOOL-TRUE]}$

$\frac{O,R⊢e_1:\text{bool}O,R⊢e_2:\text{bool}}{O,R⊢e_1\text{ and }{e}_2:\text{bool}}\text{[AND]}$
We could prove it like so: