CSE411: Introduction to Compilers

Type Checking

Jooyong Yi (UNIST)

Example

void foo() {
    int x;
    int y;
    y = x;
}

• Is the above program type-safe?

Example

void foo() {
    int i;
    char *s;
    i = s;
}

• Is the above program type-safe?

Can you give me a proof?

Is your proof machine-checkable?

Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit

Judgement

• An assertion about the typing of programs
• Syntax: Γ ⊢ J (we read this as "Γ entails J")
  • Γ: A typing environment
  • J: An assertion

[x:int][y:int] ⊢ x:int
               ⊢ (int x; int y; y = x;): unit

Revisiting Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit

Inference Rule

      Γ[I:int] ⊢ (S): unit        # premises
---------------------------
      Γ ⊢ (int I; S): unit        # conclusion  

Other Inference Rules

   Γ ⊢ I:τ  Γ ⊢ E:τ            # premises
-------------------------
   Γ ⊢ (I = E): unit           # conclusion  

Other Inference Rules

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

Other Inference Rules

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

Other Inference Rules

 Γ ⊢ S1: unit   Γ ⊢ S2: unit
-----------------------------
  Γ ⊢ (S1; S2): unit

Other Inference Rules

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

Other Inference Rules

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

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

Other Inference Rules

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

Revisiting Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit

Axioms

• Facts that are accepted as true without requiring any further justification.

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

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

How can we generate a proof tree mechanically?

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit

Implementing an Inference Rule

   Γ ⊢ I:τ  Γ ⊢ E:τ            
-------------------------
   Γ ⊢ (I = E): unit             

public boolean visit(Assignment n) {
  n.getLeftHandSide().accept(this);
  Type l = getResult();
  n.getRightHandSide().accept(this);
  Type r = getResult();
  if (l != r)
    throw new Error(n, "Type mismatch in \"" + n + "\": " + l + " = " + r);
  return false;
}

Implementing an Inference Rule

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

public boolean visit(InfixExpression n) {
  n.getLeftOperand().accept(this);
  Type l = getResult();
  n.getRightOperand().accept(this);
  Type r = getResult();
  InfixExpression.Operator o = n.getOperator();
  if (o == InfixExpression.Operator.PLUS) {
    if (l != tf.Int)
      throw new Error(n,
          "Expecting an int type expression as the left-hand operand of \""
              + o + "\" in \"" + n + "\"");
    if (r != tf.Int)
      throw new Error(n,
          "Expecting an int type expression as the right-hand operand of \""
              + o + "\" in \"" + n + "\"");
    setResult(n, tf.Int);
  }
  return false;                                                                                                          

Type Error

--------------------------      ----------------------------
 [i:int][s:char*] ⊢ i:int       [i:int][s:char*] ⊢ s:char*     
------------------------------------------------------------
                 [i:int][s:char*] ⊢ (i = s): unit              
               -------------------------------------
                 [i:int] ⊢ (char *s; i = s): unit
               ------------------------------------------------
                   ⊢ (int i; char *s; i = s): unit 

Benefits of Using Inference Rules

• Modular and compositional reasoning
  • With a finite set of rules, we can prove the correctness of any program.

Logical System

• A type-checking system is an example of a logical system.
  • A logical system consists of axioms and inference rules.

Two Fundamental Questions

1. Soundness: P ⊢ Q ⇒ P ⊧ Q
2. Completeness: P ⊧ Q ⇒ P ⊢ Q

Soundness

• ⊢ (int x; int y; y = x;): unit ⇒ ⊧ (int x; int y; y = x;): unit
• The compiler says the given program is type-safe. Is the program really type-safe?

Completeness

• ⊧ (int x; int y; y = x;): unit ⇒ ⊢ (int x; int y; y = x;): unit
• I know that the given program should be type-safe. Can the compiler prove that the program is type-safe?

Completeness

import java.util.List;
import java.util.ArrayList;

public class Incomplete {
    static class C {}
    static class D extends C {}

    public static void main(String args[]) {
        List<C> lst = new ArrayList<>();
        if (args[0].equals("1")) {
            lst.add(new D());
        } else {
            lst.add(new D());
        }
        D d = lst.get(0);
    }
}                                                                                                                   

• Is the above Java program type-safe?

Completeness

import java.util.List;
import java.util.ArrayList;

public class Incomplete {
    static class C {}
    static class D extends C {}

    public static void main(String args[]) {
        List<C> lst = new ArrayList<>();
        if (args[0].equals("1")) {
            lst.add(new D());
        } else {
            lst.add(new D());
        }
        D d = lst.get(0);
    }
}                                                                                                                   

Incomplete.java:15: error: incompatible types: C cannot be converted to D
        D d = lst.get(0);
                     ^
1 error                                                                                                          

Sound Type System: Over-approximation

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