CSE271: Principles of Programming Languages

Type Checking and Inference

Jooyong Yi (UNIST)

Type Checking

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

Type Checking Implementation

(define type-of-program
  (lambda (pgm)
    (cases program pgm
      (a-program (exp) (type-of exp (empty-tenv))))))

Type Checking for add-exp

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

(define type-of
  (lambda (exp tenv)
    (cases expression exp
      (add-exp (exp1 exp2)
        (let ((ty1 (type-of exp1 tenv))
              (ty2 (type-of exp2 tenv)))
            (check-equal-type! ty1 (int-type))   
            (check-equal-type! ty2 (int-type)) 
            (int-type)))
      ...)))              

Type Checking for if-exp

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

(define type-of
  (lambda (exp tenv)
    (cases expression exp
        (if-exp (exp1 exp2 exp3)
          (let ((ty1 (type-of exp1 tenv))
                (ty2 (type-of exp2 tenv))
                (ty3 (type-of exp3 tenv)))
            (check-equal-type! ty1 (bool-type))
            (check-equal-type! ty2 ty3)
            ty2))
      ...)))              

Type Checking for let-exp

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

(define type-of
  (lambda (exp tenv)
    (cases expression exp
        (let-exp (var exp body)
          (let ((exp-type (type-of exp tenv)))
            (type-of body
              (extend-tenv var exp-type tenv))))
      ...)))              

Type Checking for call-exp

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

(define type-of
  (lambda (exp tenv)
    (cases expression exp
        (call-exp (rator rand) 
          (let ((rator-type (type-of rator tenv))
                (rand-type  (type-of rand tenv)))
            (cases type rator-type
              (proc-type (arg-type result-type)
                (check-equal-type! arg-type rand-type)
                result-type
              (else
                (error 'unexpected-type')))))
      ...)))              

Type Checking for proc-exp

proc (x) x

• What is the type of the above procedure?

Type Checking for proc-exp

proc (x : int) x

• What is the type of the above procedure?

Type Checking for proc-exp

    (type-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑡₁]𝜏) = 𝑡₂
----------------------------------------------------------
  (type-of (proc-exp 𝑣𝑎𝑟 𝑡₁ 𝑏𝑜𝑑𝑦) 𝜏) = (𝑡₁ → 𝑡₂)

Type Checking for letrec-exp

letrec
  int double (x : int) = if zero? x
                         then 0
                         else -((double -(x, 1)), -2)
in (double 3)

Type Checking for letrec-exp

                (type-of 𝑝𝑟𝑜𝑐-𝑏𝑜𝑑𝑦 [...]𝜏) = 𝑡₁
                (type-of 𝑙𝑒𝑡𝑟𝑒𝑐-𝑏𝑜𝑑𝑦 [...]𝜏) = 𝑡₃
-----------------------------------------------------------------
  (type-of (letrec-exp 𝑡₁ 𝑝𝑟𝑜𝑐 𝑣𝑎𝑟 𝑡₂ 𝑝𝑟𝑜𝑐-𝑏𝑜𝑑𝑦 𝑙𝑒𝑡𝑟𝑒𝑐-𝑏𝑜𝑑𝑦) 𝜏) = 𝑡₃

Type Checking for letrec-exp

                (type-of 𝑝𝑟𝑜𝑐-𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑡₂, 𝑝𝑟𝑜𝑐=(𝑡₂ → 𝑡₁)]𝜏) = 𝑡₁
                (type-of 𝑙𝑒𝑡𝑟𝑒𝑐-𝑏𝑜𝑑𝑦 [𝑝𝑟𝑜𝑐=(𝑡₂ → 𝑡₁)]𝜏) = 𝑡₃
-----------------------------------------------------------------
  (type-of (letrec-exp 𝑡₁ 𝑝𝑟𝑜𝑐 𝑣𝑎𝑟 𝑡₂ 𝑝𝑟𝑜𝑐-𝑏𝑜𝑑𝑦 𝑙𝑒𝑡𝑟𝑒𝑐-𝑏𝑜𝑑𝑦) 𝜏) = 𝑡₃

Type Inference

• What would be the type of the following procedure?

 proc (f) proc (x) -((f 3), (f x))

Inferring Type Constraints

 proc (f) proc (x) -((f 3), (f x))
^                                 ^

Inferring Type Constraints

 proc (f) proc (x) -((f 3), (f x))
^                                 ^

1. t_0 = t_f → t_1

• t_0: type of proc (f) proc (x) -((f 3), (f x))
• t_f: type of f
• t_1: type of proc (x) -((f 3), (f x))

Inferring Type Constraints

proc (f) proc (x) -((f 3), (f x))
        ^                       ^

1. t_0 = t_f → t_1

• t_0: type of proc (f) proc (x) -((f 3), (f x))
• t_f: type of f
• t_1: type of proc (x) -((f 3), (f x))

2. t_1 = t_x → t_2

• t_x: type of x
• t_2: type of -((f 3), (f x))

Inferring Type Constraints

proc (f) proc (x) -((f 3), (f x))
                 ^               ^

1. t_0 = t_f → t_1

• t_0: type of proc (f) proc (x) -((f 3), (f x))
• t_f: type of f
• t_1: type of proc (x) -((f 3), (f x))

2. t_1 = t_x → t_2

• t_x: type of x
• t_2: type of -((f 3), (f x))

Inferring Type Constraints

proc (f) proc (x) -((f 3), (f x))
                 ^               ^

1. t_0 = t_f → t_1
2. t_1 = t_x → t_2
3. t_3 = int, where t_3 is the type of (f 3)
4. t_4 = int, where t_4 is the type of (f x)
5. t_2 = int

Inferring Type Constraints

proc (f) proc (x) -((f 3), (f x))
                    ^   ^

1. t_0 = t_f → t_1
2. t_1 = t_x → t_2
3. t_3 = int, where t_3 is the type of (f 3)
4. t_4 = int, where t_4 is the type of (f x)
5. t_2 = int

Inferring Type Constraints

proc (f) proc (x) -((f 3), (f x))
                    ^   ^

1. t_0 = t_f → t_1
2. t_1 = t_x → t_2
3. t_3 = int, where t_3 is the type of (f 3)
4. t_4 = int, where t_4 is the type of (f x)
5. t_2 = int
6. t_f = int → t_3

Inferring Type Constraints

proc (f) proc (x) -((f 3), (f x))
                           ^   ^

1. t_0 = t_f → t_1
2. t_1 = t_x → t_2
3. t_3 = int, where t_3 is the type of (f 3)
4. t_4 = int, where t_4 is the type of (f x)
5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → t_1
2. t_1 = t_x → t_2
3. t_3 = int
4. t_4 = int
5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → t_1
                                             2. t_1 = t_x → t_2
3. t_3 = int
4. t_4 = int
5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → (t_x → t_2)
                                             2. t_1 = t_x → t_2
3. t_3 = int
4. t_4 = int
5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → (t_x → t_2)
                                             2. t_1 = t_x → t_2
                                             3. t_3 = int
4. t_4 = int
5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → (t_x → t_2)
                                             2. t_1 = t_x → t_2
                                             3. t_3 = int
                                             4. t_4 = int
5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → (t_x → t_2)
                                             2. t_1 = t_x → t_2
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → (t_x → int)
                                             2. t_1 = t_x → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
6. t_f = int → t_3
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = t_f → (t_x → int)
                                             2. t_1 = t_x → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
6. t_f = int → int
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = (int → int) → (t_x → int)
                                             2. t_1 = t_x → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
                                             6. t_f = int → int
7. t_f = t_x → t_4

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = (int → int) → (t_x → int)
                                             2. t_1 = t_x → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
                                             6. t_f = int → int
7. int → int = t_x → int

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = (int → int) → (t_x → int)
                                             2. t_1 = t_x → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
                                             6. t_f = int → int
7. int = t_x
8. int = int

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = (int → int) → (t_x → int)
                                             2. t_1 = t_x → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
                                             6. t_f = int → int
                                             7. t_x = int
8. int = int

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = (int → int) → (int → int)
                                             2. t_1 = int → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
                                             6. t_f = int → int
                                             7. t_x = int
8. int = int

Resolving Type Constraints

Equations                                    Substitution
                                             1. t_0 = (int → int) → (int → int)
                                             2. t_1 = int → int
                                             3. t_3 = int
                                             4. t_4 = int
                                             5. t_2 = int
                                             6. t_f = int → int
                                             7. t_x = int

• What would be the type of the following procedure?

 proc (f) proc (x) -((f 3), (f x))

Another Example

 if x then -(x, 1) else 0
^                        ^ 

1. t_x = bool
2. t_1 = t_0
   • t_0: type of if x then -(x, 1) else 0
   • t_1: type of -(x, 1)
3. int = t_0

Another Example

 if x then -(x, 1) else 0
          ^      ^ 

1. t_x = bool
2. t_1 = t_0
   • t_0: type of if x then -(x, 1) else 0
   • t_1: type of -(x, 1)
3. int = t_0
4. t_x = int
5. t_1 = int

Another Example

Equations                        Substitution
1. t_x = bool
2. t_1 = t_0
3. int = t_0
4. t_x = int
5. t_1 = int

Another Example

Equations                        Substitution
                                 1. t_x = bool
2. t_1 = t_0
3. int = t_0
4. t_x = int
5. t_1 = int

Another Example

Equations                        Substitution
                                 1. t_x = bool
                                 2. t_1 = t_0
3. int = t_0
4. t_x = int
5. t_1 = int

Another Example

Equations                        Substitution
                                 1. t_x = bool
                                 2. t_1 = int
                                 3. t_0 = int
4. t_x = int
5. t_1 = int

Another Example

Equations                        Substitution
                                 1. t_x = bool
                                 2. t_1 = int
                                 3. t_0 = int
4. bool = int
5. t_1 = int

 if x then -(x, 1) else 0

Implementing Type Inference

 proc (x : ?) zero?(x)
^                     ^

(t_0 = t_x → t_1)

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (proc-exp (var otype body)
          (let ((arg-type (otype->type otype)))
☞           (cases answer (type-of body
                            (extend-tenv var arg-type tenv)
                            subst)
              (an-answer (result-type subst)
                (an-answer
                  (proc-type arg-type result-type)
                   subst)))))
      ...)))

 proc (x : ?) zero?(x)
             ^       ^

(t_1 = bool)
(t_0 = t_x → t_1)

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (zero?-exp (exp1)
☞         (cases answer (type-of exp1 tenv subst)
            (an-answer (type1 subst1)
              (let ((subst2 (unifier type1 (int-type) subst1 exp)))
                (an-answer (bool-type) subst2)))))
      ...)))

 proc (x : ?) zero?(x)
                   ^ ^

(t_1 = bool)
(t_0 = t_x → t_1)

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (var-exp (var) 
☞       (an-answer (apply-tenv tenv var) subst)) ; t_x
      ...)))

 proc (x : ?) zero?(x)
              ^      ^

[t_x = int]
(t_1 = bool)
(t_0 = t_x → t_1)

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (zero?-exp (exp1)
          (cases answer (type-of exp1 tenv subst)
            (an-answer (type1 subst1) ; type1 = t_x
☞             (let ((subst2 (unifier type1 (int-type) subst1 exp))) ; subst2 = (t_x . (int-type))
                (an-answer (bool-type) subst2)))))
      ...)))

 proc (x : ?) zero?(x)
              ^      ^

[t_x = int]
t_1 = bool
(t_0 = t_x → t_1)

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (zero?-exp (exp1)
          (cases answer (type-of exp1 tenv subst)
            (an-answer (type1 subst1) ; type1 = t_x
              (let ((subst2 (unifier type1 (int-type) subst1 exp))) ; subst2 = (t_x . (int-type))
☞               (an-answer (bool-type) subst2)))))
      ...)))

 proc (x : ?) zero?(x)
^                     ^

[t_x = int]
t_0 = t_x → bool

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (proc-exp (var otype body)
          (let ((arg-type (otype->type otype))) ; arg-type = t_x
            (cases answer (type-of body
                            (extend-tenv var arg-type tenv)
                            subst)
              (an-answer (result-type subst) ; result-type = bool-type                              
☞               (an-answer
                  (proc-type arg-type result-type)
                   subst)))))
      ...)))

 proc (x : ?) zero?(x)

[t_x = int]
t_0 = t_x → bool

  (define type-of-program
    (lambda (pgm)
      (cases program pgm
        (a-program (exp1)
          (cases answer (type-of exp1 (init-tenv) (empty-subst))
            (an-answer (ty subst) ; ty = t_x → bool, subst = [t_x = int]
              (apply-subst-to-type ty subst))))))) ; int → bool

Another Example

 proc (f : ?) proc (x : ?) -((f 3), (f x))
^                                        ^

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (proc-exp (var otype body)
          (let ((arg-type (otype->type otype)))
☞           (cases answer (type-of body
                            (extend-tenv var arg-type tenv)
                            subst)
              (an-answer (result-type subst)
                (an-answer
                  (proc-type arg-type result-type)
                   subst)))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
             ^                           ^

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (proc-exp (var otype body)
          (let ((arg-type (otype->type otype)))
☞           (cases answer (type-of body
                            (extend-tenv var arg-type tenv)                         
                            subst)
              (an-answer (result-type subst)
                (an-answer
                  (proc-type arg-type result-type)
                   subst)))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                          ^              ^

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (diff-exp (exp1 exp2)
☞         (cases answer (type-of exp1 tenv subst)
            (an-answer (type1 subst1)
              (let ((subst1 (unifier type1 (int-type) subst1 exp1)))                             
                (cases answer (type-of exp2 tenv subst1)
                  (an-answer (type2 subst2)
                    (let ((subst2
                            (unifier type2 (int-type) subst2 exp2)))
                      (an-answer (int-type) subst2))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                             ^   ^

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (call-exp (rator rand)
☞         (let ((result-type (fresh-tvar-type))) ; result-type = t_1                               
            (cases answer (type-of rator tenv subst)
              (an-answer (rator-type subst)
                (cases answer (type-of rand tenv subst)
                  (an-answer (rand-type subst)
                    (let ((subst
                            (unifier rator-type
                              (proc-type rand-type result-type)
                              subst
                              exp)))
                      (an-answer result-type subst))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                             ^   ^

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (call-exp (rator rand)
          (let ((result-type (fresh-tvar-type))) ; result-type = t_1                                
            (cases answer (type-of rator tenv subst)
☞             (an-answer (rator-type subst) ; rator-type = t_f
                (cases answer (type-of rand tenv subst)
                  (an-answer (rand-type subst)
                    (let ((subst
                            (unifier rator-type
                              (proc-type rand-type result-type)
                              subst
                              exp)))
                      (an-answer result-type subst))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                             ^   ^

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (call-exp (rator rand)
          (let ((result-type (fresh-tvar-type))) ; result-type = t_1                                
            (cases answer (type-of rator tenv subst)
              (an-answer (rator-type subst) ; rator-type = t_f
                (cases answer (type-of rand tenv subst)
☞                 (an-answer (rand-type subst) ; rand-type = int
                    (let ((subst
                            (unifier rator-type
                              (proc-type rand-type result-type)
                              subst
                              exp)))
                      (an-answer result-type subst))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                             ^   ^

[t_f = int → t_{(f 3)}]                                                  

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (call-exp (rator rand)
          (let ((result-type (fresh-tvar-type))) ; result-type = t_{(f 3)}                                
            (cases answer (type-of rator tenv subst)
              (an-answer (rator-type subst) ; rator-type = t_f
                (cases answer (type-of rand tenv subst)
                  (an-answer (rand-type subst) ; rand-type = int
                    (let ((subst
☞                           (unifier rator-type
                              (proc-type rand-type result-type)
                              subst
                              exp)))
                      (an-answer result-type subst))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                          ^              ^

[t_f = int → t_{(f 3)}]      →      [t_f = int → int]
[type_{(f 3)} = int]                [type_{(f 3)} = int]                          

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (diff-exp (exp1 exp2)
          (cases answer (type-of exp1 tenv subst)
            (an-answer (type1 subst1) ; type1 = type_{(f 3)}
☞             (let ((subst1 (unifier type1 (int-type) subst1 exp1)))                             
                (cases answer (type-of exp2 tenv subst1)
                  (an-answer (type2 subst2)
                    (let ((subst2
                            (unifier type2 (int-type) subst2 exp2)))
                      (an-answer (int-type) subst2))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                                    ^   ^

[t_f = int → int]        
[type_{(f 3)} = int]                                          

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (call-exp (rator rand)
          (let ((result-type (fresh-tvar-type))) ; result-type = t_{(f x)}                                
            (cases answer (type-of rator tenv subst)
              (an-answer (rator-type subst) ; rator-type = t_f
                (cases answer (type-of rand tenv subst)
                  (an-answer (rand-type subst) ; rand-type = t_x
                    (let ((subst
☞                           (unifier rator-type
                              (proc-type rand-type result-type)
                              subst
                              exp)))
                      (an-answer result-type subst))))))))
      ...)))

[t_{(f x)} = int]
[t_x = int]
[t_f = int → int]        
[type_{(f 3)} = int]                                          

(define unifier
  (lambda (typ1 typ2 subst exp)
    ;; typ1 = t_f, typ2 = t_x → t__{(f x)}                                                                   
    (let ((ty1 (apply-subst-to-type typ1 subst))  ; ty1 = int → int
          (ty2 (apply-subst-to-type typ2 subst))) ; ty2 = t_x → t_{(f x)}
      (cond
        ...
        ((and (proc-type? ty1) (proc-type? ty2))
           (let ((subst2 (unifier
                          (proc-type->arg-type ty1)
                          (proc-type->arg-type ty2)
                          subst exp)))  ; [t_x = int]
             (let ((subst3 (unifier
                             (proc-type->result-type ty1)
                             (proc-type->result-type ty2)
                             subst2 exp))) ; [t_{(f x)} = int]
               subst3)))
        ...))))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
                          ^              ^

[t_{(f x)} = int]
[t_x = int]
[t_f = int → int]        
[type_{(f 3)} = int]                                          

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (diff-exp (exp1 exp2)
          (cases answer (type-of exp1 tenv subst)
            (an-answer (type1 subst1) ; type1 = type_{(f 3)}
              (let ((subst1 (unifier type1 (int-type) subst1 exp1)))                             
                (cases answer (type-of exp2 tenv subst1)
                  (an-answer (type2 subst2) ; type2 = type_{(f x)}
☞                   (let ((subst2
                            (unifier type2 (int-type) subst2 exp2)))
                      (an-answer (int-type) subst2))))))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
             ^                           ^

[t_{(f x)} = int]
[t_x = int]
[t_f = int → int]        
[type_{(f 3)} = int]                                          

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (proc-exp (var otype body)
          (let ((arg-type (otype->type otype))) ; arg-type = t_x
            (cases answer (type-of body
                            (extend-tenv var arg-type tenv)                         
                            subst)
              (an-answer (result-type subst) ; result-type = int                           
☞               (an-answer         
                  (proc-type arg-type result-type) ; t_x → int
                   subst)))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))
^                                        ^

[t_{(f x)} = int]
[t_x = int]
[t_f = int → int]        
[type_{(f 3)} = int]                                          

(define type-of
  (lambda (exp tenv subst)
    (cases expression exp
      (proc-exp (var otype body)
          (let ((arg-type (otype->type otype))) ; arg-type = t_f
            (cases answer (type-of body
                            (extend-tenv var arg-type tenv)
                            subst)
              (an-answer (result-type subst) ; result-type = t_x → int                          
☞               (an-answer
                  (proc-type arg-type result-type) ; t_f → (t_x → int)
                   subst)))))
      ...)))

 proc (f : ?) proc (x : ?) -((f 3), (f x))

subst:
[t_{(f x)} = int]
[t_x = int]
[t_f = int → int]        
[type_{(f 3)} = int]                                          

  (define type-of-program
    (lambda (pgm)
      (cases program pgm
        (a-program (exp1)
          (cases answer (type-of exp1 (init-tenv) (empty-subst))                                   
            (an-answer (ty subst) ; ty = t_f → (t_x → int)
              (apply-subst-to-type ty subst))))))) ; (int → int) → (int → int)