Typechecking

15‐411/15‐611 Compiler Design

Seth Copen Goldstein

October 8, 2019
 Compiler Phases
source
code
Abstract syntax tree

Lex Parse Semantics translation

AST+symbol tables

Intermediate Representation (tree)

instruction register code

optimization
selection allocation generation

Code Triples

15‐411/611 2
 Today
• Types & Type Systems
• Type Expressions
• Type Equivalence
• Type Checking

15‐411/611 3
 Types
• A type is a set of values and a set of operations
that can be performed on those values.
– E.g, int in c0 is in [‐231,231)
– bool in C0 is in { false, true }

15‐411/611 4
 Types & Typesystems
• A type is a set of values and a set of operations
that can be performed on those values.
• A Typesystem is a set of rules which assign types
to expressions, statements, and thus the entire
program
– what operations are valid for which types
– Concise formalization of the checking rules
– Specified as rules on the structure of expressions, …
– Language specific

15‐411/611 5
 Static vs Dynamic Types
• Static type: type assigned to an expression
at compile time
• Dynamic type: type assigned to a storage
location at run time
• Statically typed language: static type
assigned to every expression at compile
time
• Dynamically typed language: type of an
expression determined at run time
• Untyped language: no typechecking, e.g.,
assembly
15‐411/611 7
 Why Static Typing?
• Compiler can reason more effectively
• Allows more efficient code: don’t have to
check for unsupported operations
• Allows error detection by compiler
• Documents code!
• But:
– requires at least some type declarations
– type decls often can be inferred (ML, C+11)

15‐411/611 8
 Dynamic checks
• Array index out of bounds
• null in Java, null pointers in C
• Inter‐module type checking in Java
• Sometimes can be eliminated through
static analysis (but usually harder than type
checking)

15‐411/611 9
 Sound Type System
• If an expression is assigned type t, and it
evaluates to a value v, then v is in the set of
values defined by t
• IOW, dynamic type of expression (at
runtime) is the static type of the expression
(derived at compiled time)

• SML, OCAML, Scheme and Ada have sound

type systems
• Most implementations of C and C++ do not
15‐411/611 10
 Strongly Typed Language
• When no application of an operator to
arguments can lead to a run‐time type
error, language is strongly typed
• strongly typed != statically typed

15‐411/611 11
 Strongly Typed Language
• C++ claimed to be “strongly typed”, but
– Union types allow creating a value of one
type and using it at another
– Type coercions may cause unexpected
(undesirable) effects
– No array bounds check (in fact, no
runtime checks at all)
• SML, OCAML “strongly typed” but still
must do dynamic array bounds checks,
runtime type case analysis, and other
checks

15‐411/611 12
 Limitations
• Can still have runtime errors:
– division by zero
– exceptions
• Static type analysis has to be conservative,
thus some “correct” programs will be
rejected.

15‐411/611 13
 Example: c0 type system
• Language type systems have primitive types
(also: basic types, atomic types)
• C0: int, bool, char, string
• Also have type constructors that operate on
types to produce other types
• C0: for any type T, T [ ], T* is a type.
• Extra types: void denotes absence of value

15‐411/611 15
 Type Expressions
• Type expressions are used in declarations
and type casts to define or refer to a type
– Primitive types, such as int and bool
– Type constructors, such as pointer‐to, array‐of,
records and classes, templates, and functions
– Type names, such as typedefs in C and named
types in Pascal, refer to type expressions

15‐411/611 16
 Type expressions: aliases
• Some languages allow type aliases (e.g.,
type definitions)
– C: typedef int int_array[ ];
– Modula‐3: type int_array = array of int;
• int_array is type expression denoting same
type as int [ ] ‐‐ not a type constructor

15‐411/611 17
 Type Expressions: Arrays
• Different languages have various kinds of
array types
• w/o bounds: array(T)
– C, Java: T[ ], Modula‐3: array of T
• size: array(T, L) (may be indexed 0..L‐1)
– C: T[L], Modula‐3: array[L] of T
• upper & lower bounds: array(T,L,U)
– Pascal, Modula‐3: indexed L..U
• Multi‐dimensional arrays (FORTRAN)

15‐411/611 18
 Records/Structures

• More complex type constructor

• Has form {id1: T1, id2: T2, …} for some ids
and types Ti
• Supports access operations on each field,
with corresponding type
• C: struct { int a; float b; } corresponds to
type {a: int, b: float}
• Class types (e.g. Java) extension of record
types
15‐411/611 19
 Functions

• Some languages have first‐class function types (C,

ML, Modula‐3, Pascal, not Java)
• Function value can be invoked with some
argument expressions with types Ti, returns
return type Tr.
• Type: T1T2  …  TnTr
• C: int f(float x, float y)
– f: float  float  int
• Function types useful for describing methods, as
in Java, even though not values, but need
extensions for exceptions.
15‐411/611 20
 Type Equivalence
• Name equivalence: Each distinct type name
is a distinct type.
• Structural Equivalence: two types are
identical if they have the same structure

15‐411/611 21
 Name Equivalence
• Each type name is a distinct type, even
when the type expressions the names refer
to are the same
• Types are identical only if names match
• Used by Pascal (inconsistently)

type link = ^node; Using name equivalence:

var next : link; p ≠ next
last : link; p ≠ last
p : ^node; p = q = r
q, r : ^node; next = last

15‐411/611 22
 Structural Equivalence
• Two types are the same if they are
structurally identical
• Used in C0, C, Java

typedef node* link;

link next;
link last;
node* p;
node* q;
Using structural equivalence:

p = q = next = last

15‐411/611 23
 Representing Types

int *f(char*,char*)

fun fun

args pointer args pointer

pointer pointer int pointer int

char char char

Tree forms DAGs

15‐411/611 24
 Representing Types

int *f(char*,char*)

fun fun

args pointer args pointer

pointer pointer int pointer int

char char char

Tree forms DAGs

15‐411/611 25
 Cyclic Graph Representations

struct Node
{
int val;
struct Node *next;
};

struct

val next

int pointer

Cyclic graph
15‐411/611 26
 Structural Equivalence (cont’d)
• Two structurally equivalent type
expressions have the same pointer address
when constructing graphs by sharing nodes

struct Node
{
int val; struct
struct Node *next; val next
};
int pointer

15‐411/611 27
 Structural Equivalence (cont’d)
• Two structurally equivalent type
expressions have the same pointer address
when constructing graphs by sharing nodes

struct Node
s
{
int val; struct
struct Node *next; val next
};
int pointer
struct Node s, *p;
p

15‐411/611 28
 Structural Equivalence (cont’d)
• Two structurally equivalent type
expressions have the same pointer address
when constructing graphs by sharing nodes
*p
struct Node
s
{
int val; struct
struct Node *next; val next
};
int pointer
struct Node s, *p;
p
… p = &s; // OK &s
… *p = s; // OK
15‐411/611 29
 Constructing Type Graphs
• Construct over AST (or during parse)

type  int $$ = getIntType();

| bool $$ = getBoolType();
| * type $$ = makePtrType($2);
| type [ num ] $$ = makeArrayType($1, $3);
typedef  typedef type id install($3,$2);

• Invariant: Same structural type is same

pointer.

15‐411/611 30
 Type Checking
• When is op(arg1,…,argn) allowed?
• Type checking ensures 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

15‐411/611 31
 Type Checking
• Type checking may be done statically
at compile time or dynamically at run
time
• Dynamically typed languages (eg LISP,
Prolog, javascript) do only dynamic
type checking
• Statically typed languages can do most
type checking statically

15‐411/611 32
 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

15‐411/611 33
 Dynamic Type Checking
• Data object must contain type information
• Errors aren’t detected until violating
application is executed
• May introduce extra overhead at runtime.
• Can make code hard to read
• Supposedly, easier to prototype code

15‐411/611 34
 Static Type Checking
• Performed after parsing, before code
generation
• Type of every variable and signature of
every operator must be known at
compile time

15‐411/611 35
 Static Type Checking
• Can eliminate need to store type
information in data object if no
dynamic type checking is needed
• Catches many programming errors at
earliest point
• Can’t check types that depend on
dynamically computed values
– Eg: array bounds

15‐411/611 36
 Static Type Checking
• Typically places restrictions 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

15‐411/611 37
 Type Inference
• Type inference: A program analysis to
assign a type to an expression from
the program context 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

15‐411/611 38
 Format of Type Judgments
• A type judgement has the form
 |‐ exp : 
•  is a typing environment
– Supplies the types of variables and functions
–  is a set of the form { x : , . . . }
– For any x at most one  such that (x :   )
• exp is a program expression
•  is a type to be assigned to exp
• |‐ pronounced “turnstyle”, or “entails” (or
“satisfies” or, informally, “shows”)

15‐411/611 39
 Axioms - Constants

 |‐ n : int (assuming n is an integer constant)

 |‐ true : bool  |‐ false : bool

• These rules are true with any typing environment

• , n are meta‐variables

15‐411/611 40
 Axioms – Variables

Notation: Let (x) =  if x :   

Variable axiom:

(x) = 
 |‐ x : 

15‐411/611 41
 Simple Rules - Arithmetic
Primitive operators (   { +,*, &&, …}):

 |‐ e1:  |‐ e2:
 |‐ e1  e2 : 

 is a type variable, i.e., it can take any type but

all instances of  must be the same.

15‐411/611 42
 Simple Rules – Relational Ops
Relations (  { < , > , ==, <=, >= }):
˜

 |‐ e1 :   |‐ e2 : 
 |‐ e1 e2 :bool
˜
Do we know what  is here?

15‐411/611 43
 Example: {x:int} |- x + 2 = 3 :bool

What do we need to show first?

{x:int} |‐ x + 2 = 3 : bool

15‐411/611 44
 Example: {x:int} |- x + 2 = 3 :bool

What to do on left side?

{x : int} |‐ x + 2 : int {x:int} |‐ 3 :int

{x:int} |‐ x + 2 = 3 : bool

15‐411/611 45
 Example: {x:int} |- x + 2 = 3 :bool

Almost Done

{x:int} |‐ x:int {x:int} |‐ 2:int

{x : int} |‐ x + 2 : int {x:int} |‐ 3 :int
{x:int} |‐ x + 2 = 3 : bool

15‐411/611 46
 Example: {x:int} |- x + 2 = 3 :bool

Complete Proof (type derivation)

(x) = int
{x:int} |‐ x:int {x:int} |‐ 2:int
{x : int} |‐ x + 2 : int {x:int} |‐ 3 :int
{x:int} |‐ x + 2 = 3 : bool

15‐411/611 47
 Simple Rules - Booleans
Connectives
 |‐ e1 : bool  |‐ e2 : bool
 |‐ e1 && e2 : bool

 |‐ e1 : bool  |‐ e2 : bool
 |‐ e1 || e2 : bool

15‐411/611 48
 Function Application

• Application rule:
 |‐ e1 : 1  2  |‐ e2 : 1
 |‐ e1(e2) : 2

• If you have a function expression e1 of type

1  2 applied to an argument e2 of type
1, the resulting expression e1(e2) has type
2

15‐411/611 49
 What about statements?

• Statements don’t have types.

• But, they result in a function returning a
value with a type.
• If a function returns type , then we say s
is well typed if,
 |‐ s[]

15‐411/611 50
 What about statements?

15‐411/611 52
 Effect on 

15‐411/611 53
 Shadowing?

xdom()

15‐411/611 54
 Function Rule
• Rules describe types, but also how the
environment  may change

, {f:12 , x : 1 } |‐ s [2]
 |‐ 2 f(1 x) s

15‐411/611 55
 Implementing rules
• Start from goal judgments for each
function
 |– ( id ( ..., ai : Ti, ... ) : T = E )
• Work backward applying inference rules to
sub‐trees of abstract syntax trees
• Exactly the same kind of recursive traversal
as last week

15‐411/611 60
 Other Issues
• What to do with types after typechecking?
– decorate AST?
– Typed IR?
– Typed triples?
• What to do on errors?
– uninitialized variable?
– undeclared variable?
– wrong return type?
– wrong operator type?

15‐411/611 61