CSE411: Introduction to Compilers

Type Checking 1

Jooyong Yi (UNIST)

Interface of a Type Checker

      |--------------|           
AST → | Type Checker | → ok / error
      |--------------|         

Interpreting a Type-Checking Error

      |--------------|           
AST → | Type Checker | → error
      |--------------|         

• The given program ____ have a type error.
• That is, there ____ exist an input that causes a type error.

Interpreting Type-Checking Success

      |--------------|           
AST → | Type Checker | → ok
      |--------------|         

• The given program ____ be type-safe.
• That is, there ____ not exist an input that causes a type error.

Type Error

• What is a type error?
• How do we define a type error?

What Do We Need?

• Type Rules: The rules (or constraints) that should be satisfied by a type-safe program
• A proof system: An inference system that can be used to prove that a program satisfies the type rules

Type Proof Example

------------------------   ------------------------
Γ[x:int][y:int] ⊢ y:int    Γ[x:int][y:int] ⊢ x:int
-------------------------------------------------------
                Γ[x:int][y:int] ⊢ y = x;
               ------------------------------
                Γ[x:int] ⊢ int y; y = x;
               ------------------------------
                  Γ ⊢ int x; int y; y = x;

Judgement

• A basic ingredient of a type rule
• An assertion about the typing of programs
• Syntax: Γ ⊢ J (we read this as "Γ entails J")
  • Γ: A static typing environment (no runtime information is included)
  • J: An assertion

Examples of Judgement

Γ ⊢ int x; x = 0;     # int x; x = 0; is well-typed in Γ
Γ ⊢ x:int             # x has an int type in Γ

Type Rule: Assignment

   Γ ⊢ I:τ  Γ ⊢ E:τ       # premises
----------------------
      Γ ⊢ I = E           # conclusion  

• When all of the premises are satisfied, the conclusion must hold.

Type Rule: Statement Sequence

      Γ[I:int] ⊢ S
----------------------
      Γ ⊢ int I; S            

# When S1 is not a variable declaration

  Γ ⊢ S1    Γ ⊢ S2
---------------------- 
      Γ ⊢ S1; S2

Type Rule: Variable in Environment

--------------
 Γ[x:τ] ⊢ x:τ

• No premises are used. Such a rule is called an axiom.
• An axiom expresses a fact that is always true.

Type Rule: If Statements

 Γ ⊢ E: boolean   Γ ⊢ S
--------------------------
  Γ ⊢ if (E) S

Type Rule: While Statements

 Γ ⊢ E: boolean   Γ ⊢ S
--------------------------
  Γ ⊢ while (E) S

Type Rule: Arithmetic Expressions

   Γ ⊢ E1: int   Γ ⊢ E2: int
------------------------------
      Γ ⊢ E1 + E2: int

Type Rule: Equality

    Γ ⊢ E1: τ   Γ ⊢ E2: τ
------------------------------
      Γ ⊢ E1 == E2: boolean

Type Rule: Procedure Invocation

   Γ ⊢ P: τ_1 × τ_2 × ... × τ_n → τ   Γ ⊢ E_k: τ_k (for k = 1, ..., n)
 -----------------------------------------------------------------------
           Γ ⊢ P(E1, E2, ..., En): τ

Type Rule: Integer Constant

-----------------
  Γ ⊢ n: int        # n is an integer constant

Type Derivation

-----------------   --------------------
Γ[x:int] ⊢ x:int     Γ[x:int] ⊢ 10:int
-------------------------------------------
         Γ[x:int] ⊢ x = 10;
    ------------------------------
         Γ ⊢ int x; x = 10;

• Root: a given program
• Each judgment is obtained from the ones immediately above it by some type rule.

Well-Typed Program

-----------------   --------------------
Γ[x:int] ⊢ x:int     Γ[x:int] ⊢ 10:int
-------------------------------------------
         Γ[x:int] ⊢ x = 10;
    ------------------------------
         Γ ⊢ int x; x = 10;

• A program is well-typed if a valid proof tree is obtained.
• A proof tree is valid if all leaves are axioms and all internal nodes are obtained by applying a type rule.
• A type error occurs when a valid proof tree cannot be obtained.

Type Soundness

• A sound type system guarantees that a well-typed program is type-safe.
• It is guaranteed that no type rule will be violated at runtime, no matter what input is given.

Type Soundness

• Most statically typed languages use a sound type system.
  • If a compiler accepts a program, then the program is guaranteed to be type-safe.
  • This is one of the benefits of using a statically typed language.

Statically Typed but Unsound

• Go is a statically typed language.
• The following program is accepted by the Go compiler, but it is not type-safe.

package main

import "fmt"

type foo interface {}

func main() {
	var i foo = "hello"

	s := i.(string) // check if i is a string at runtime
	fmt.Println(s)

	f = i.(float64) // runtime error
	fmt.Println(f)
}

Type Soundness

• Most dynamically typed languages cannot guarantee the type soundness of the programs.

Interpreting Type-Checking Success

      |--------------|           
AST → | Type Checker | → ok
      |--------------|         

• The given program must be type-safe if the type system is sound.
• That is, there must not exist an input that causes a type error.

Interpreting a Type-Checking Error

      |--------------|           
AST → | Type Checker | → error
      |--------------|         

• The given program ____ have a type error.
• That is, there ____ exist an input that causes a type error.

Interpreting a Type-Checking Error

• Can a type error occur in the following program?

int x;
x = 10;
if (false) x = true;

Interpreting a Type-Checking Error

• Can a type error occur in the following program?

int x;
x = 10;
if (false) x = true;

• Most compilers report a type error.

Our Type System

• Our type system also rejects the program.

                                     Γ[x:int] ⊢ x:int  Γ[x:int] ⊢ true: boolean     # wrong premise
       ---------------------------  --------------------------------------------- 
         Γ[x:int] ⊢ false: boolean    Γ[x:int] ⊢ x = true
       ----------------------------------------------------  
         Γ[x:int] ⊢ if (false) x = true;
    ----------------------------------------------
         Γ ⊢ int x; if (false) x = true;

Revisit the Type Rule for If Statements

• The rule does not provide special treatment for the case where E is always false.

 Γ ⊢ E: boolean   Γ ⊢ S
--------------------------
  Γ ⊢ if (E) S

Sound Type System: Over-approximation

• A sound type system may reject some programs that are type-safe.