CSE411: Introduction to Compilers

Type Inference

Jooyong Yi (UNIST)

Type Inference Example

main() {
   var x, y, z;
   x = 10;
   y = alloc 8; // allocate 4 bytes of memory containing 8
   *y = x;
   z = *y;
   return x;  
}

• Is this program type-safe?
• What are the types of x, y and z?

Type Inference Example

• Notations
  • 〚x〛= τ means the type of x is τ.
  • ↑ τ means a pointer to τ.

main() {
   var x, y, z;
   x = 10;           // 〚x〛= int
   y = alloc 8;      // 〚y〛= 〚alloc 8〛= ↑〚8〛= ↑ int
   *y = x;           // 〚y〛= ↑〚x〛= ↑ int
   z = *y;           // 〚z〛= 〚*y〛, 〚y〛= ↑〚*y〛
   return x;  
}

Type Inference Rules

main() {
   var x, y, z;
   x = 10;           // 〚x〛= int
   y = alloc 8;      // 〚y〛= 〚alloc 8〛= ↑〚8〛= ↑ int
   *y = x;           // 〚y〛= ↑〚x〛= ↑ int
   z = *y;           // 〚z〛= 〚*y〛, 〚y〛= ↑〚*y〛
   return x;                                                                                                             
}

Collecting Type Constraints

main() {
   var x, y, z;
   x = 10;           // {〚x〛= 〚10〛, 〚10〛= int}
   y = alloc 8;      // {〚y〛= 〚alloc 8〛, 〚alloc 8〛= ↑〚8〛, 〚8〛= int}
   *y = x;           // {〚y〛= ↑〚x〛} 
   z = *y;           // {〚z〛= 〚*y〛, 〚y〛= ↑〚*y〛} 
   return x;                                                                                                             
}

Solving Type Constraints

main() {
   var x, y, z;
   x = 10;           // {〚x〛= 〚10〛, 〚10〛= int}
   y = alloc 8;      // {〚y〛= 〚alloc 8〛, 〚alloc 8〛= ↑〚8〛, 〚8〛= int}
   *y = x;           // {〚y〛= ↑〚x〛} 
   z = *y;           // {〚z〛= 〚*y〛, 〚y〛= ↑〚*y〛} 
   return x;                                                                                                             
}

• The problem we want to solve:
  • 〚x〛= __, 〚y〛= __, 〚z〛= __ ⊢ type constraints

Unification Problem

Unification Problem

• Given two terms T1 and T2, find a substitution σ such that σ(T1) = σ(T2).
  • Example 1: When T1 = 〚10〛, T2 = int, σ = {〚10〛→ int}
  • Example 2: When T1 =〚x〛, T2 =〚10〛, σ = {〚x〛→ int, 〚10〛→ int}
  • Example 3: When T1 = ↑〚x〛, T2 = ↑〚*y〛, σ = {〚x〛→ int, *y → int}

What If?

main() {
   var x, y, z;
   x = 10;           // {〚x〛= 〚10〛, 〚10〛= int}
   // y = alloc 8;   
   y = 42;
   *y = x;           // {〚y〛= ↑〚x〛} 
   z = *y;           // {〚z〛= 〚*y〛, 〚y〛= ↑〚*y〛} 
   return x;                                                                                                             
}

Logical Reasoning

• Induction
• Deduction
• Abduction

Logical Reasoning

• Induction
  • examples ⊢ claim
• Deduction
  • rules ⊢ claim
• Abduction
  • ?? ⊢ claim

Type Inference for Dynamic Languages

• Is static type checking and static type inference possible for dynamic languages?
• Does it even make sense?

Type Inference for Dynamic Languages

def find_match(color): str -> Optional[str]
  candidates = get_colors()
  for candidate in candidates:
    if candidate == color:
      return candidate
  return None    

• Deduction
• Abduction
• Induction + Abduction