CSE411

CSE411: Introduction to Compilers

Type Inference

Jooyong Yi (UNIST)

2026 Fall
CSE411

Type Inference Example

fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;
    y = Box::new(8);
    *y = x;
    z = *y;
    x
}
  • Is this program type-safe?
  • What are the types of x, y and z?
2026 Fall
CSE411

Type Inference Example

  • Notations
    • 〚x〛= τ means the type of x is τ.
    • Box(τ) means an owning pointer to a value of type τ.
fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;          // 〚x〛 = i32
    y = Box::new(8); // 〚y〛 = 〚Box::new(8)〛 = Box(〚8〛)
    *y = x;          // 〚y〛 = Box(〚x〛)
    z = *y;          // 〚z〛 = 〚*y〛, 〚y〛 = Box(〚*y〛)
    x                // 〚x〛 = i32
}
2026 Fall
CSE411

Type Inference Rules

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;          // 〚x〛 = i32
    y = Box::new(8); // 〚y〛 = 〚Box::new(8)〛 = Box(〚8〛)
    *y = x;          // 〚y〛 = Box(〚x〛)
    z = *y;          // 〚z〛 = 〚*y〛, 〚y〛 = Box(〚*y〛)
    x                // 〚x〛 = i32
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2
    *E
    fn f() -> T { ... E }
2026 Fall
CSE411

Type Inference Rules

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;          // 〚x〛 = i32
    y = Box::new(8); // 〚y〛 = 〚Box::new(8)〛 = Box(〚8〛)
    *y = x;          // 〚y〛 = Box(〚x〛)
    z = *y;          // 〚z〛 = 〚*y〛, 〚y〛 = Box(〚*y〛)
    x                // 〚x〛 = i32
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E
    fn f() -> T { ... E }
2026 Fall
CSE411

Type Inference Rules

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;          // 〚x〛 = i32
    y = Box::new(8); // 〚y〛 = 〚Box::new(8)〛 = Box(〚8〛)
    *y = x;          // 〚y〛 = Box(〚x〛)
    z = *y;          // 〚z〛 = 〚*y〛, 〚y〛 = Box(〚*y〛)
    x                // 〚x〛 = i32
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E }
2026 Fall
CSE411

Type Inference Rules

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;          // 〚x〛 = i32
    y = Box::new(8); // 〚y〛 = 〚Box::new(8)〛 = Box(〚8〛)
    *y = x;          // 〚y〛 = Box(〚x〛)
    z = *y;          // 〚z〛 = 〚*y〛, 〚y〛 = Box(〚*y〛)
    x                // 〚x〛 = i32
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Collecting Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;
    y = Box::new(8);
    *y = x;
    z = *y;
    x
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Collecting Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);
    *y = x;
    z = *y;
    x
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Collecting Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;
    z = *y;
    x
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Collecting Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;           // {〚y〛= Box(〚x〛)}
    z = *y;
    x
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Collecting Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;           // {〚y〛= Box(〚x〛)}
    z = *y;           // {〚z〛= 〚*y〛, 〚y〛= Box(〚*y〛)}
    x
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Collecting Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;           // {〚y〛= Box(〚x〛)}
    z = *y;           // {〚z〛= 〚*y〛, 〚y〛= Box(〚*y〛)}
    x                 // {〚x〛= i32 }
}
  • Construct Rule
    X = E 〚X〛= 〚E〛
    10 〚10〛= i32
    Box::new(E) 〚Box::new(E)〛= Box(〚E〛)
    *E1 = E2 〚E1〛= Box(〚E2〛)
    *E 〚E〛= Box(〚*E〛)
    fn f() -> T { ... E } 〚E〛 = T
2026 Fall
CSE411

Solving Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;           // {〚y〛= Box(〚x〛)}
    z = *y;           // {〚z〛= 〚*y〛, 〚y〛= Box(〚*y〛)}
    x                 // {〚x〛= i32 }
}

  • 〚x〛= ?, 〚y〛= ?, 〚z〛= ?

2026 Fall
CSE411

Solving Type Constraints

Constraints:

{〚x〛= 〚10〛, 
 〚10〛= i32,
 〚y〛= 〚Box::new(8)〛, 
 〚Box::new(8)〛= Box(〚8〛), 
 〚8〛= i32,
 〚y〛= Box(〚x〛),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛),
 〚x〛= i32 }
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{〚x〛= 〚10〛, ←
 〚10〛= i32,
 〚y〛= 〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(〚x〛),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛),
 〚x〛= i32 }

 ↓

{〚10〛=〚10〛,
 〚10〛= i32,
 〚y〛= 〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(〚10〛),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛),
 〚10〛= i32 }     

 ↓

{〚10〛= i32,
 〚y〛= 〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(〚10〛),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛),
 〚10〛= i32 }     

  • Substitutions:

{〚x〛⟼〚10〛}
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{〚10〛= i32, ←
 〚y〛= 〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(〚10〛),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛),
 〚10〛= i32 }     

 ↓

{ i32 = i32,
 〚y〛= 〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(i32),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛),
  i32 = i32 }     

↓

{〚y〛= 〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(i32),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛)}         

  • Substitutions:

{〚x〛⟼〚10〛,
 〚10〛⟼ i32}

↓

{〚x〛⟼ i32,
 〚10〛⟼ i32}
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{〚y〛= 〚Box::new(8)〛, ←
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚y〛= Box(i32),
 〚z〛= 〚*y〛,
 〚y〛= Box(〚*y〛) }     

 ↓

{〚Box::new(8)〛=〚Box::new(8)〛,
 〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚Box::new(8)〛= Box(i32),
 〚z〛= 〚*y〛,
 〚Box::new(8)〛= Box(〚*y〛) }     

 ↓

{〚Box::new(8)〛= Box(〚8〛),
 〚8〛= i32,
 〚Box::new(8)〛= Box(i32),
 〚z〛= 〚*y〛,
 〚Box::new(8)〛= Box(〚*y〛) }          

  • Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ 〚Box::new(8)〛}
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{〚Box::new(8)〛= Box(〚8〛), ←
 〚8〛= i32,
 〚Box::new(8)〛= Box(i32),
 〚z〛= 〚*y〛,
 〚Box::new(8)〛= Box(〚*y〛) }     

 ↓

{ Box(〚8〛) = Box(〚8〛),
 〚8〛= i32,
  Box(〚8〛)= Box(i32),
 〚z〛= 〚*y〛,
  Box(〚8〛) = Box(〚*y〛)}     

 ↓

{〚8〛= i32,
  Box(〚8〛)= Box(i32),
 〚z〛= 〚*y〛,
  Box(〚8〛) = Box(〚*y〛)}           

  • Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼〚Box::new(8)〛,
 〚Box::new(8)〛⟼ Box(〚8〛) }

 ↓
 
{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(〚8〛),
 〚Box::new(8)〛⟼ Box(〚8〛) }
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{〚8〛= i32, ←
  Box(〚8〛)= Box(i32),
 〚z〛= 〚*y〛,
  Box(〚8〛) = Box(〚*y〛) }     

 ↓

{ i32 = i32,
  Box(i32)= Box(i32),
 〚z〛= 〚*y〛,
  Box(i32) = Box(〚*y〛) }     
  
 ↓

{〚z〛= 〚*y〛,
  Box(i32) = Box(〚*y〛) }     

  • Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(〚8〛),
 〚Box::new(8)〛⟼ Box(〚8〛),
 〚8〛⟼ i32 }
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{〚z〛=〚*y〛, ←
  Box(i32) = Box(〚*y〛) }     
 ↓

{〚*y〛=〚*y〛,
  Box(i32) = Box(〚*y〛) }     

 ↓

{ Box(i32) = Box(〚*y〛) }     

  • Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(i32),
 〚Box::new(8)〛⟼ Box(i32),
 〚8〛⟼ i32,
 〚z〛⟼〚*y〛 }
2026 Fall
CSE411

Solving Type Constraints

  • Constraints:

{ Box(i32) = Box(〚*y〛) }     

 ↓

{ Box(i32) = Box(i32) }     

 ↓

{ }     

  • Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(i32),
 〚Box::new(8)〛⟼ Box(i32),
 〚8〛⟼ i32,
 〚z〛⟼〚*y〛,
 〚*y〛⟼ i32 }    

 ↓

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(i32),
 〚Box::new(8)〛⟼ Box(i32),
 〚8〛⟼ i32,
 〚z〛⟼ i32,
 〚*y〛⟼ i32 }
2026 Fall
CSE411

Solving Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;           // {〚y〛= Box(〚x〛)}
    z = *y;           // {〚z〛= 〚*y〛, 〚y〛= Box(〚*y〛)}
    x                 // {〚x〛= i32 }
}

Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(i32),
 〚Box::new(8)〛⟼ Box(i32),
 〚8〛⟼ i32,
 〚z〛⟼ i32,
 〚*y〛⟼ i32 }

  • 〚x〛= ?, 〚y〛= ?, 〚z〛= ?

2026 Fall
CSE411

Solving Type Constraints

  • fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;           // {〚x〛= 〚10〛, 〚10〛= i32 }
    y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                      //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    *y = x;           // {〚y〛= Box(〚x〛)}
    z = *y;           // {〚z〛= 〚*y〛, 〚y〛= Box(〚*y〛)}
    x                 // {〚x〛= i32 }
}

Substitutions:

{〚x〛⟼ i32,
 〚10〛⟼ i32,
 〚y〛⟼ Box(i32),
 〚Box::new(8)〛⟼ Box(i32),
 〚8〛⟼ i32,
 〚z〛⟼ i32,
 〚*y〛⟼ i32 }

  • 〚x〛= i32, 〚y〛= Box(i32),
    〚z〛= i32

2026 Fall
CSE411

Unification Algorithm

  • Input: A set of type constraints C
  • Output: A substitution σ or failure
  • Repeatedly select a constraint T₁ = T₂:
Condition Action
T₁ = T₂ (identical terms) Remove the constraint
T₁ is a type variable σ' = {T₁ ↦ T₂} ∘ σ
T₁ is not a type variable and T₂ is a type variable σ' = {T₂ ↦ T₁} ∘ σ
Box(A) = Box(B) C' = {A = B} ∪ C
Otherwise Fail
  • Occurs check: Reject α ↦ T if α occurs in T.
  • Apply each substitution to the remaining constraints.
  • When all constraints are solved, return the composed substitution σ.
2026 Fall
CSE411

What If?

fn main() -> i32 {
    let x;
    let mut y;
    let z;

    x = 10;              // {〚x〛=〚10〛, 〚10〛= i32 }
    // y = Box::new(8);  // {〚y〛= 〚Box::new(8)〛, 
                         //  〚Box::new(8)〛= Box(〚8〛), 〚8〛= i32 }
    y = 42;              // {〚y〛=〚42〛, 〚42〛= i32 }
    *y = x;              // {〚y〛= Box(〚x〛)}
    z = *y;              // {〚z〛= 〚*y〛, 〚y〛= Box(〚*y〛)}
    x
}
2026 Fall

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

--- # Unification vs. Anti-Unification | | Unification | Anti-Unification | |---|---|---| | Goal | Find a common instance | Find a common generalization | | Input | T₁, T₂ | T₁, T₂ | | Output | Substitution σ | Term G and substitutions σ₁, σ₂ | | Condition | σ(T₁) = σ(T₂) | σ₁(G) = T₁, σ₂(G) = T₂ | | Optimal result | Most General Unifier (MGU) | Least General Generalization (LGG) | **Unification example** - T₁ = Box(α), T₂ = Box(i32) - σ = {α ↦ i32} - Common instance: Box(i32) **Anti-unification example** - T₁ = Box(i32), T₂ = Box(bool) - G = Box(α) - σ₁ = {α ↦ i32}, σ₂ = {α ↦ bool} **Unification specializes; anti-unification generalizes.**