Lambda Calculus Type inference examples

1] \ x -> x
 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.