A Guideline for Homework 33

Exercise 4.16.1

Infer the type of this expression:

proc (f,g,p,x)
     if (p (f x))
       then (g 1 x)
       else add1((f x))

This is what we know (we will denote the type of a given expression as t:<exp>):

• t:proc = ( t:f * t:g * t:p * t:x -> t:body )

So the result is a proc-type with four type parameters and a return type.
To determine the final result, we must determine the type of each of the four parameters, and the type of the proc's body.  So we add the following five statements to our list of items to solve:

• t:f = ( t:x -> ? )
• t:g = ( t:1 * t:x -> ? )
• t:p = ( t:(f x) -> ? )
• t:x = ?
• t:body = t:if (p (f x)) then (g 1 x) else add1((f x))

We discover types by recursing through the AST.

1. We can immediately infer that t:1 is an int.  So we now know that:

   • t:g = ( int * t:x -> ? )

2. What we know about t:if is:

   • t:test-exp = bool
   • t:true-exp = t:false-exp
   • t:if = t:true-exp = t:false-exp

   So we substitute those expressions into the equation:

   • t:test-exp = t:(p (f x)) = bool
   • t:if is the same type as t:true-exp = t:(g 1 x) which is the same type as t:false-exp = t:add1((f x))

   p must return a bool.
   add1 takes an int as a parameter, thus f must return an int.
   add1 returns an int, thus g must return an int.
   f returns an int, thus p must take an int.
   t:true-exp = t:false-exp = int, thus t:body = t:if = int.
   We can now make the following substitutions (shown in red):

   • t:f = ( t:x -> int )
   • t:g = ( int * t:x -> int )
   • t:p = ( int -> bool )
   • t:x = ?
   • t:body = int

Since there are no other inferences that we can make in this expression, we conclude that it is polymorphic in x, and the final answer is:

t:proc = ( ( t:x -> int ) * ( int * t:x -> int ) * ( int -> bool ) * t:x -> int )