BEGIN 16_11_01_ConstraintsForTypeInference.lhs

Continuation of 16_10_27_ConstraintsForTypeInference.lhs
_________________________________________

EXAMPLE 4

> h x = x

Associate unknown type T1 to h, unknown type T2 to x, and unknown type
T3 to (h x). 
    
    h      :: T1
    x      :: T2
    (h x)  :: T3

In this case we have two constraints:

    T1 = T2 -> T3    because h is applied to x

    T3 = T2          because the types of the two side in the definition,
                     (h x) and x, must be equal

We have to find a UNIFIER in order to solve these two constraints. Skipping
the details shown in the previous 16_10_27_ConstraintsForTypeInference.lhs,
the desired unifier here is:

    U (T1) = a -> a
    U (T2) = a
    U (T3) = a

where 'a' is a type variable.
     
END EXAMPLE 4
_________________________

EXAMPLE 5

Set up the constraints for the following definition:

> h' = \ x -> x

then find a unifier U to solve the constraints, and then use U to infer
the principal type (or most general type) of h'.

END EXAMPLE 5
_______________________

EXAMPLE 6

Set up the constraints for the following definition:

> f_twice = let f = (\ x -> x) in (f f)

     f_twice                      :: T1
     f                            :: T2
     x                            :: T3
     (\x -> x)                    :: T4
     (f f)                        :: T5
     let f = (\ x -> x) in (f f)  :: T6

The constraints are:

     T4 = T3 -> T3    because of the abstraction '(\x -> x)'
     T2 = T2 -> T5    because of the application '(f f)'
     T2 = T4          because of the inner (local) binding 'f = (\x -> x)'
     T5 = T6          because the type of 'let ...' must equal the type of '(f f)'
     T1 = T6          because of the outer binding 'f_twice = let ...'    

Consider the second constraint T2 = T2 -> T5. Is there a unifier U such that:

     U(T2) = U(T2 -> T5)   or   U(T2) = U(T2) -> U(T5)

The answer is NO. Why? However, the definition of f_twice type-checks according
to the Haskell interpreter. So, what gives?

HINT: Polymorphism.

END EXAMPLE 6

END 16_11_01_ConstraintsForTypeInference.lhs