Above function takes one argument and returns the same argument as result, therefore type of argument and return value must be same.
type: a - > a
2] \ x y -> x
Above function takes two arguments and returns the first argument as result, therefore type of first argument and return value must be same.
type: a -> b -> a
3] \f g -> g (f g)
Above function takes two parameter f and g.
To solve this, my algorithm is as follows:
First look at function body from right-to-left. Function body is g(f g)
Assume type of g is t1. That is, ( g = t1).
Now, take next variable from function body, which is f. f is a function that take g as argument and return value of any type, say return type is a. So far, there is no restriction of return value of f. assume type of f is t1-> a. That is, (f = t1 -> a).
Now, take next variable, which is g. g is a function that takes return value of function f as a argument (a), and returns value of any type, say return type is b. So far there is no restriction of type of value return by g. But we already assume g is of type t1. Now, we found that g is function so, t1 is a - > b.
That is, (g = g = t1 = a -> b).
Now replace t1 in f with (a -> b). So f becomes f = (a -> b ) -> a
we have done with function body. Now look at function declaration syntax. It takes two arguments f and g, and f is first argument, g is second argument, and return value is of same type of return value of g.
So type of function \f g -> g (f g) is as follows:
((a -> b) -> a) -> ( a -> b) -> b
4] \ x f g -> f g (x g)
Above function accepts three arguments x, f and g.
Assume g is of type a. that is, (g = a).
Now, x takes g as a argument and returns any type of value. So far there is no restriction on type of value returned by x, say return type of value is b.
Therefore, x = a -> b
Now, f takes two argument g and return type of x. Return type of f has no restriction, so say it is of type c.
Therefore, f = a -> b -> c
(Note: For simplicity as assume g as a variable. And is of type a. However, you can consider it g as a function then you have to unify a = d->e and replace all occurrences of a with d->e)
Return type of f is the return type of this function.
Now look at function definition and arrange its type accordingly.
\ x f g -> f g (x g) type is as follows:
(a -> b) -> (a -> b -> c) -> a - > c
5] \ f g x -> f ( g x)
Above function takes three arguments, namely, f , g ,and x.
Assume x is of type a., That is ( x = a)
Now g takes x as argument and returns a value. Assume return type of g is b.
Therefore, (g = a -> b)
Now f takes return value of g as argument (that is, b) and returns a value.
Therefore, ( f = b -> c)
So type of \f g x -> f (g x) is:
Now, look at function declaration: \f g x
(b -> c) -> (a -> b) -> a ->c
6] \x y f -> f (x (\w -> f w)) (y f x)
Above function takes three arguments, x y and f.
Now look at Function body, and assume type for each variable.
Let w = a
x = t1
y = t2
f = t3
Observe the function body, f will be applied to on first argument (x (\w -> f x)), and then it will be applied on second argument (y f x).
Go inside \w function,
f = t3 = a - > b
Therefore, x = t1 = (a -> b) -> c
Return type of x is c, which will become the argument of f, therefore unification is possible here, and c = a;
Hence, x = t1 = (a->b) ->a
Now we examine ( y f x) part,
y = t2 = (a -> b) -> (a->b->a) -> d
d is the return type of y.
After applying the first argument (x(\w->f w)), f returns b.
Therefore, d is parameter of b.
b should take d as argument and return a value, That is, b = d -> e
Now replace each occurrence of b with d -> e
f = a -> b = a -> d -> e
x = (a ->b -> a ) = ((a -> d -> e)- > a)
y = (a ->d -> e) -> ( a -> d -> e) -> a) -> d
Hence type of entire expression is, (arrenge according to function definition:
((a -> d -> e)- > a) ->
(a ->d -> e) -> ( a -> d -> e) -> a) -> d ->
(a -> d -> e) -> e
e is the return type of entire expression which is also the return type of f.