BEGIN 16_10_27_ConstraintsForTypeInference.lhs

EXAMPLE 1

> absolute :: Int -> Int
> absolute x = abs x 

> f x = (absolute y) + z 
>        where
>       (y,z) = x 

The following is equivalent to the preceding:

> g x = let (y,z) = x 
>       in  (+) (absolute y) z 

Assuming that absolute :: Int -> Int and (+) :: Int -> Int -> Int,

HOW TO DISCOVER THE TYPE OF 'g' ?

We will discover the type of 'g' in two stages:

STAGE 1: We set up CONSTRAINTS between the yet-to-be-determined types 
      (i.e. type variables) of all the subexpressions in the definition of 'g'.

STAGE 2: We resolve the CONSTRAINTS from Stage 1 by defining a UNIFIER,
      which is a function that substitutes type expressions into all
      the type variables.

ELABORATING STAGE 1:
-------------------

All the subexpressions in the definition of 'g' with their corresponding 
type variables:
 
   g                     :: T1
   x                     :: T2
   y                     :: T3
   z                     :: T4
   absolute              :: T5
   (+)                   :: T6
   (g x)                 :: T7
   (y,z)                 :: T8
   (absolute y)          :: T9
   (+) (absolute y)      :: T10
   (+) (absolute y) z    :: T11

We set up the CONSTRAINTS by parsing and inspecting the program code. 
Because g :: T1 and x :: T2 and (g x) :: T7, we have the CONSTRAINT:

   T1 = T2 -> T7

Because y :: T3 and z :: T4 and (y,z) = x, we have the CONSTRAINT:

   T8 = (T3,T4) 

Because (y,z) = x, we have the CONSTRAINT:

   T2 = T8 

Because absolute :: Int -> Int, by assumption, we have the CONSTRAINT:

   T5 = Int -> Int

Because 'absolute' is applied to 'y', and absolute :: T5 and y :: T3, we have 
the CONSTRAINT:

   T5 = T3 -> T9 

Because (+) :: Int -> Int -> Int, by assumption, we have the CONSTRAINT:

   T6 = Int -> Int -> Int

Because (+) is applied to (absolute y), we have the CONSTRAINT:

   T6 = T9 -> T10

Because '(+) (absolute y)' is applied to z, we have the CONSTRAINT:

   T10 = T4 -> T11

Finally, because the type of the left-hand-side in the definition of 'g'
must equal the type of the right-hand-side, we have the CONSTRAINT:

   T7 = T11

CONCLUSION FOR STAGE 1:
---------------------- 

For every construct in the program code, we have a constraint:
    4 applications corresponding to 4 constraints
    1 pairing corresponding to 1 constraint
    2 equations corresponding to 2 constraints
for a total of 7 constraints.

ELABORATING STAGE 2:
-------------------

The UNIFIER will be a function of the form:

   U : { T1, T2, ... , T11 } -> { type expressions }

which SUBSTITUTES for each type variable an appropriate type expression.

From the constraint T5 = Int -> Int, we immediately have the SUBSTITUTION:

   U(T5) = Int -> Int

From the constraint T6= Int -> Int -> Int, we immediately have the SUBSTITUTION:

   U(T6) = Int -> Int -> Int

From the constraint T5 = T3 -> T9, we have the equation:

   U(T5) = U(T3 -> T9) = U(T3) -> U(T9)

which implies the two SUNSTITUTIONS:

   U(T3) = Int  and   U(T9) = Int

From the constraint  T6 = T9 -> T10, we have the equation:

   U(T6) = U(T9 -> T10) = U(T9) -> U(T10)

which implies the two substitutions:

   U(T9) = Int   and   U(T10) = Int -> Int

From the constraint T10 = T4 -> T11, we have the equation:

   U(T10) = U(T4 -> T11) = U(T4) -> U(T11) 

which implies the two substitutions:

   U(T4) = Int   and   U(T11) = Int

From the constraint T8 = (T3,T4), we have the equation:

   U(T8) = U(T3,T4) = ( U(T3),U(T4) )

which implies the substitutions:

   U(T8) = (Int,Int)

From the constraint T2 = T8, we have the equation:

   U(T2) = U(T8)

which implies the substitution:

   U(T2) = (Int,Int)

From the constraint T7 = T11, we have the equation:

   U(T7) = U(T11)

which implies the substitution:

   U(T7) = Int

Finally, from the constraint T1 = T2 -> T7, we have the equation:

   U(T1) = U(T2 -> T7) = U(T2) -> U(T7)

which implies the substitution:

   U(T1) = (Int,Int) -> Int

CONCLUSION FOR STAGE 2:
----------------------

We have resolved all the constraints by defining the following
substitutions:

   T1  := (Int,Int) -> Int
   T2  := (Int,Int)
   T3  := Int
   T4  := Int
   T5  := Int -> Int
   T6  := Int -> Int -> Int
   T7  := Int
   T8  := (Int,Int)
   T9  := Int
   T10 := Int -> Int
   T11 := Int

END EXAMPLE 1

EXAMPLE 2

We use a slightly adjusted version of the code in Example 1:

> g2 x = let (y,z) = x 
>        in  (+) y z 

We leave it to you to set up the CONSTRAINTS (Stage 1) and then
find a UNIFIER (Stage 2) to resolve the constraints.

END EXAMPLE 2

EXAMPLE 3

Another slightly adjusted version of the code in Example 1, but
this one will not type-check:

  g3 x = let (y,z) = x 
         in  (+) (y,z) z 

We leave it to you to set up the CONSTRAINTS (Stage 1) and then
discover that there is no UNIFIER (Stage 2) that will resolve
the constraints.

END EXAMPLE 3


END 16_10_27_ConstraintsForTypeInference.lhs