Types and Type Systems

March 1, 2024
All notes are expanded based on

Why Data Types?

---

• Data types play a key role in:
• $\text{Data abstraction}$ in the design of programs
• $\text{Type checking}$ in the analysis of programs
• $\text{Compile-time code generation}$ in the translation and execution of programs
• Data layout (how many words; which are data and which are pointers) dictated by type

Terminology

---

• Type: A $\text{type}\text{t}$ defines a set of ppssible data values
• E.g. $\text{short}$ in C is $\{x\mid 2^{15}-1\ge x\ge -2^{15}\}$
• A value in this set is said to have type $t$

• Type system: rules of a language assigning types to expressions

Types as Specifications

---

• Types describe properties
• Different type systems describe different properties, e.g.
• Data is read write-versus read-only
• Operation has authority to access data
• Data came from right source
• Operation might or could not raise an exception
• Common type systems focus on types describing same data layout and access methods

Sound Type System

---

• If an expression is assigned type $\text{t}$, and it evaluates toa value $\text{v}$, then $\text{v}$ is in the set of values defined by $\text{t}$
• SML, OCAML, Scheme and Ada have sound type systems
• Most implementations of C and C++ do not

Strongly Typed Language

---

• When no appliaction of an operator to arguments can lead to a run-time type error, langauge is $\text{stronly typed}$
• E.g. 1 + 2.3;;
• Depends on definition of type error
• C++ claimed to be strongly typed, but
• Union types allow creating a value at one type and using it at another
• Type coercions may cause unexpected (underirable) effects
• No array bounds check (in fact, no runtime checks at all)
• SML, OCAML strongly type but still must do dynamic array bounds checks, runtime type case analysis, and other checks

Static vs Dynamic Types

---

• $\text{Static type}:$ type assigned to an expression at compile time
• $\text{Dynamic type}:$ type assigned to a storage location at run time
• $\text{Statically typed language}:$ static type assigned to every expression at compile time
• $\text{Dynamically typed language}:$ type of an expression determined ar run time

Type Checking

---

• When is op(arg1, …, argn) allowed?
• $\text{Type checking}$ assures that operations are applied to the right number of arguments of the right types
• Right type may mean same type as was specified, or may mean that there is a predefined implicit coercion that will be applied
• Used to resolve overloaded operations
• Type checking may be done $\text{statically}$ at compile time or $\text{dynimically}$ at run time
• Dynamically typed (aka untyped) languages (e.g. LISP, Prolog) do only dynamic type checking
• Statically typed languages can do most typed checking statically

Dynamic Type Checking

---

• Performed at run-time before each operation is applied
• Types of variables and operations left unspecified until run-time
• Same variable may be used at different types
• Data object must contain type information
• Errors aren’t detected until violating application is execurted (maybe years after the code was written)

Static Type Checking

---

• Performed after parsing, before code generation
• Type of every variable and signature of every operator must be known at compile time
• Can eliminate need to store type information in data object if no dynamic type checking is needed
• Catches many programming arrors at earliest point
• Can’t check types that depend on dynamically computed values
• E.g. array bounds
• Typically places restriction on languages
• Garbage collection
• References instead of pointers
• All variables initialized when created
• Variable only used at one type
• Union types allow for work-arounds, but effectively introduce dynamic type checks

Type Declarations

---

• $\text{Type declarations}:$ explicit assigment of types to variables (signatures to functios) in the code of a program
• Must be checked in a strongly typed language
• Often not necessary for strong typing or even static typing (depends on the type system)

Type Inference

---

• $\text{Type inference}:$ A program analysis to assign a type to an expression from the program cobtext of the expression
• Fully static type inference first introduced by Robin Miller in ML
• Haskle, OCAML, SML all use type inference
• Records are a problem for type inference

Format of Type Judgments

---

• A $\text{type judgement}:$ has the form
$$\mathrm{\Gamma }⊢\text{ exp }:\tau$$

• $\mathrm{\Gamma }$ is typing environment
• Supplies the types of variables (and function names when function names are not variables)
• $\mathrm{\Gamma }$ is a set of the form $\{x:\sigma ,...\}$
• For any $x$ at most on $\sigma$ such that $(x:\sigma \in \mathrm{\Gamma })$
• $\text{exp}$ is a program expression
• $\tau$ is a type to be assigned to $\text{exp}$
• $⊢$ pronounced “turnstyle”, or “entails” (or satisfies or, informally, shows)

Axioms - Constants (Monomorphic)

---

$\frac{}{\mathrm{\Gamma }⊢n:int}$ (assuming $n$ is an integer constant)

$$\frac{}{\mathrm{\Gamma }⊢\text{ true }:\text{ bool }}\frac{}{\mathrm{\Gamma }⊢\text{ false }:\text{ bool }}$$

• These rules are true with any typing environmnet
• $\mathrm{\Gamma },n$ are meta-variables

Axioms - Variables (Monomorphic Rule)

---

Notation: Let $\mathrm{\Gamma }(x)=\sigma$ if $x:\sigma \in \mathrm{\Gamma }$ Note: if such $\sigma$ exits, its unique

Variable axiom:

$$\frac{}{\mathrm{\Gamma }⊢x:\sigma }\text{ if }\mathrm{\Gamma }(x)=\sigma$$

Simple Rules - Arithmetic (Mono)

---

Primitive Binary operators $(\oplus \in \{+,-,\ast ,...\}):$

$$\frac{\mathrm{\Gamma }⊢e_1:{\tau }_1\mathrm{\Gamma }⊢e_2:{\tau }_2(\oplus ):{\tau }_1\to {\tau }_2\to {\tau }_3}{\mathrm{\Gamma }⊢e_1\oplus e_2:{\tau }_3}$$

Special case: Relations $(\sim \in \{<,>,=,<=,>=\})$:

$$\frac{\mathrm{\Gamma }⊢e_1:\tau \mathrm{\Gamma }⊢e_2:\tau (\sim ):\tau \to \tau \to \text{ bool }}{\mathrm{\Gamma }⊢e_1\sim e_2:\text{ bool }}$$

$$\text{For the moment, think }\tau \text{ is int}$$

Example: $\{x:\text{int}\}⊢x+2=3:\text{ bool}$

---

What do we need to show first?

What we need fot the left and right side?

How to finish?

And

Complete Proof (type derivation)

$$\text{Bin}\frac{\text{Bin}\frac{\text{Var}\frac{}{\{x:\text{int}\}⊢x:\text{int}}\text{Const}\frac{}{\{x:\text{int}\}⊢2:\text{int}}}{\{x:\text{int}\}⊢x+2:\text{int}}\text{Const}\frac{}{\{x:\text{int}\}⊢3:\text{int}}}{\{x:\text{int}\}⊢x+2=3:\text{int}}$$

Simple Rules - Booleans

---

Connectives

$$\frac{\mathrm{\Gamma }⊢e_1:\text{bool}\mathrm{\Gamma }⊢e_2:\text{bool}}{\mathrm{\Gamma }⊢e_1\mathrm{\&}\mathrm{\&}{e}_2:\text{ bool}}$$

$$\frac{\mathrm{\Gamma }⊢e_1:\text{bool}\mathrm{\Gamma }⊢e_2:\text{bool}}{\mathrm{\Gamma }⊢e_1||e_2:\text{ bool}}$$

Type Variables in Rules

---

• If-then-else rule:

$$\frac{\mathrm{\Gamma }⊢e_1:\text{ bool }\mathrm{\Gamma }⊢e_2:\tau \mathrm{\Gamma }⊢e_3:\tau }{\mathrm{\Gamma }⊢(\text{if }{e}_1\text{ then }{e}_2\text{ else }{e}_3)\tau }$$

• $\tau$ is a type variable (meta-variable)
• Can take any type at all
• All instances in a rule application must get same type
• Then branch, else branch and if-then-else must all have same type

Example derivation: if-then-else:

---

$\mathrm{\Gamma }=\{x:\text{int, int\_of\_float : float }\to \text{ int, y : float }\}$