CSE271: Principles of Programming Languages

Types

Jooyong Yi (UNIST)

Interpreter

                                   Input to P
                                       ↓
Program P → [Front End] → AST → [ Interpreter ]
                                       ↓
                                   Output of P

Example

1 + "2"

Type Error Example

1 + "2"

TypeError: unsupported operand type(s) for +: 'int' and 'str'

Type Error Example

1 + "2"

TypeError: unsupported operand type(s) for +: 'int' and 'str'

• Where does the type error occur?

                                   Input to P
                                       ↓
Program P → [Front End] → AST → [ Interpreter ]
                                       ↓
                                   Output of P

Review

• How do we interpret (+ 1 2)?

Review

(define value-of
  (lambda (exp env)
     (cases expression exp
        (add-exp (exp1 exp2)
          (let ((val1 (value-of exp1 env))
                (val2 (value-of exp2 env)))
            (let ((num1 (expval->num val1))
                  (num2 (expval->num val2)))
              (num-val (+ num1 num2)))))))
     ...)              

Review

  (value-of 𝑒𝑥𝑝₁ ρ) = (num-val 𝑛𝑢𝑚₁)    (value-of 𝑒𝑥𝑝₂ ρ) = (num-val 𝑛𝑢𝑚₂) 
----------------------------------------------------------------------------
          (value-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ) = (num-val (+ 𝑛𝑢𝑚₁ 𝑛𝑢𝑚₂))

Question

• What is the type of (+ 1 2)?

Question

• What is the type of (+ 1 2)?

  (type-of 𝑒𝑥𝑝₁ 𝜏) = ...    (type-of 𝑒𝑥𝑝₂ 𝜏) = ...
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = ...

Question

• What is the type of (+ 1 2)?

  (type-of 𝑒𝑥𝑝₁ 𝜏) = int    (type-of 𝑒𝑥𝑝₂ 𝜏) = int
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = int

When do we report a type error?

(+ 1 "2")

  (type-of 𝑒𝑥𝑝₁ 𝜏) = int    (type-of 𝑒𝑥𝑝₂ 𝜏) = int
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = int

Type-Checking Impl for add-exp

(define value-of
  (lambda (exp env)
     (cases expression exp
        (add-exp (exp1 exp2)
          (let ((val1 (value-of exp1 env))
                (val2 (value-of exp2 env)))    → 	
            (let ((num1 (expval->num val1))
                  (num2 (expval->num val2)))
              (num-val (+ num1 num2)))))))
      ...)              

Type-Checking Impl for add-exp

(define value-of                                     (define type-of
  (lambda (exp env)                                    (lambda (exp tenv)
     (cases expression exp                                (cases expression exp
        (add-exp (exp1 exp2)                                (add-exp (exp1 exp2)
          (let ((val1 (value-of exp1 env))                     (let ((ty1 (type-of exp1 tenv))
                (val2 (value-of exp2 env)))    →                     (ty2 (type-of exp2 tenv)))
            (let ((num1 (expval->num val1))                      (int-type)))
                  (num2 (expval->num val2)))               ...)))
              (num-val (+ num1 num2)))))
      ...)))              

Type-Checking Impl for add-exp

(define value-of                                     (define type-of
  (lambda (exp env)                                    (lambda (exp tenv)
     (cases expression exp                                (cases expression exp
        (add-exp (exp1 exp2)                                (add-exp (exp1 exp2)
          (let ((val1 (value-of exp1 env))                     (let ((ty1 (type-of exp1 tenv))
                (val2 (value-of exp2 env)))    →                     (ty2 (type-of exp2 tenv)))
            (let ((num1 (expval->num val1))                       (check-equal-type! ty1 (int-type))   
                  (num2 (expval->num val2)))                      (check-equal-type! ty2 (int-type)) 
              (num-val (+ num1 num2)))))                          (int-type)))
      ...)))                                               ...)))

(define check-equal-type!
    (lambda (ty1 ty2)
      (when (not (equal? ty1 ty2))
        (report-unequal-types ty1 ty2))))

Typing Rule for add-exp

  (type-of 𝑒𝑥𝑝₁ 𝜏) = int    (type-of 𝑒𝑥𝑝₂ 𝜏) = int
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = int

Typing Rule for const-exp

  (type-of (const-exp 𝑛𝑢𝑚) 𝜏) = int

Typing Rule for var-exp

  (type-of (var-exp 𝑣𝑎𝑟) 𝜏) = 𝜏(𝑣𝑎𝑟)

Typing Rule for zero?

    (type-of 𝑒𝑥𝑝 𝜏) = int
--------------------------------------
  (type-of (zero?-exp 𝑒𝑥𝑝) 𝜏) = bool

Typing Rule for if-exp

    (type-of 𝑒𝑥𝑝₁ 𝜏) = bool    (type-of 𝑒𝑥𝑝₂ 𝜏) = t    (type-of 𝑒𝑥𝑝₃ 𝜏) = t
------------------------------------------------------------------------------
                  (type-of (if-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂ 𝑒𝑥𝑝₃) 𝜏) = t

Typing Rule for let-exp

    (type-of 𝑒𝑥𝑝 𝜏) = 𝑡₁    (type-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑡₁]𝜏) = 𝑡₂
----------------------------------------------------------
         (type-of (let-exp 𝑣𝑎𝑟 𝑒𝑥𝑝 𝑏𝑜𝑑𝑦) 𝜏) = 𝑡₂

Typing Rule for call-exp

    (type-of 𝑟𝑎𝑡𝑜𝑟 𝜏) = (𝑡₁ → 𝑡₂)    (type-of 𝑟𝑎𝑛𝑑 𝜏) = 𝑡₁
----------------------------------------------------------------------------
          (type-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) 𝜏) = 𝑡₂

Quizzes

• What is the type of 3?

Quizzes

• What is the type of zero? 3?

    (type-of 𝑒𝑥𝑝 𝜏) = int
--------------------------------------
  (type-of (zero?-exp 𝑒𝑥𝑝) 𝜏) = bool

Quizzes

• What is the type of proc (x) (+ x 1)?

Quizzes

• What is the type of proc (x) (+ x 1)?
  • (int → int)

Quizzes

• What is the type of proc (x) if x then 11 else 22?

Quizzes

• What is the type of proc (x) if x then 11 else 22?
  • (bool → int)

Quizzes

• What is the type of proc (x) proc (y) if y then x else 22?

Quizzes

• What is the type of proc (x) proc (y) if y then x else 22?
  • (int → (bool → int))

Quizzes

• What is the type of proc (f) if (f 3) then 11 else 22?

Quizzes

• What is the type of proc (f) if (f 3) then 11 else 22?
  • ((int → bool) → int)

Type Checking

                                                     Input to P
                                                         ↓
Program P → [Front End] → AST → [ Type Checker ] → [ Interpreter ]
                                                         ↓
                                                     Output of P

Static vs. Dynamic Typing

                                                     Input to P
                                                         ↓
Program P → [Front End] → AST → [ Type Checker ] → [ Interpreter ]
                                                         ↓
                                                     Output of P

                                           Input to P
                                               ↓
Program P → [Front End] → AST → [ Type Checker + Interpreter ]
                                               ↓
                                           Output of P

Type Checker vs. Interpreter

  (value-of 𝑒𝑥𝑝₁ ρ) = (num-val 𝑛𝑢𝑚₁)    (value-of 𝑒𝑥𝑝₂ ρ) = (num-val 𝑛𝑢𝑚₂) 
----------------------------------------------------------------------------
          (value-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ) = (num-val (+ 𝑛𝑢𝑚₁ 𝑛𝑢𝑚₂))

  (type-of 𝑒𝑥𝑝₁ 𝜏) = int    (type-of 𝑒𝑥𝑝₂ 𝜏) = int
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = int

Type Checker vs. Interpreter

• A type checker runs the program with abstract values.

  (value-of 𝑒𝑥𝑝₁ ρ) = (num-val 𝑛𝑢𝑚₁)    (value-of 𝑒𝑥𝑝₂ ρ) = (num-val 𝑛𝑢𝑚₂) 
----------------------------------------------------------------------------
          (value-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ) = (num-val (+ 𝑛𝑢𝑚₁ 𝑛𝑢𝑚₂))

  (type-of 𝑒𝑥𝑝₁ 𝜏) = int    (type-of 𝑒𝑥𝑝₂ 𝜏) = int
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = int

Type Checker vs. Interpreter

• A type checker runs the program with abstract values.
  • This makes it possible to consider all possibilities without running the program.

  (value-of 𝑒𝑥𝑝₁ ρ) = (num-val 𝑛𝑢𝑚₁)    (value-of 𝑒𝑥𝑝₂ ρ) = (num-val 𝑛𝑢𝑚₂) 
----------------------------------------------------------------------------
          (value-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ) = (num-val (+ 𝑛𝑢𝑚₁ 𝑛𝑢𝑚₂))

  (type-of 𝑒𝑥𝑝₁ 𝜏) = int    (type-of 𝑒𝑥𝑝₂ 𝜏) = int
----------------------------------------------------------------------------
          (type-of (+ 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) 𝜏) = int

Type Safety

• If a type checker does not report a type error, does it mean the program is type-safe, meaning it will not encounter a type error when run?

                                                     Input to P
                                                         ↓
Program P → [Front End] → AST → [ Type Checker ] → [ Interpreter ]
                                                         ↓
                                                     Output of P

Type Safety

• If a type checker does not report a type error, does it mean the program is type-safe, meaning it will not encounter a type error when run?
  • The answer is yes, if the type checker is sound.

Soundness

• ⊢ E: 𝜏 ⇒ ⊧ E: 𝜏

Question

• Can a type checker catch all type errors?

Question

• Can a type checker catch all type errors?
  • Yes, if the type checker is sound.
  • ⊢ E: 𝜏 ⇒ ⊧ E: 𝜏
  • ¬ ⊧ E: 𝜏 ⇒ ¬ ⊢ E: 𝜏

Soundness and Completeness

• Soundness: ⊢ E: 𝜏 ⇒ ⊧ E: 𝜏
• Completeness: ⊧ E: 𝜏 ⇒ ⊢ E: 𝜏

Completeness

• Completeness: ⊧ E: 𝜏 ⇒ ⊢ E: 𝜏
• Suppose we know that E has type 𝜏. Can a type checker always correctly derive the type of E to 𝜏?

Completeness

• Completeness: ⊧ E: 𝜏 ⇒ ⊢ E: 𝜏
• Suppose we know that E has type 𝜏. Can a type checker always correctly derive the type of E to 𝜏?
• Can a type checker always prove that a type-safe program is type-safe?

Consider C

• Is the type checker for C sound?

Consider C

• Is the type checker for C sound?

double d = 3.14;
int i = d;

Rust

let d:f64 = 3.14; // equivalent to double d = 3.14;
let i:i32 = d;    // equivalent to int i = d;

Quizz

• What is the type of proc (x) if x then 11 then zero? 3?

Quizz

• What is the type of proc (x) if x then 11 then zero? 3?

    (type-of 𝑒𝑥𝑝₁ 𝜏) = bool    (type-of 𝑒𝑥𝑝₂ 𝜏) = t    (type-of 𝑒𝑥𝑝₃ 𝜏) = t
------------------------------------------------------------------------------
                  (type-of (if-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂ 𝑒𝑥𝑝₃) 𝜏) = t

Question

• Can we have a type checker that is both sound and complete?

Question

• Can we have a type checker that is both sound and complete?
  • This is proven to be impossible.

Sound and Incomplete or Complete and Unsound

• Which type checker would you prefer?

  • Soundness: ⊢ E: 𝜏 ⇒ ⊧ E: 𝜏
  • Completeness: ⊧ E: 𝜏 ⇒ ⊢ E: 𝜏

Sound Type System: Over-approximation

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