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

**. Function body is**

*right-to-left***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:

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**.

It is a good post on Lambda Calculus. Nice work.

ReplyDeleteGood post but you could have showed what's happening when you try your algorithm on something like \f -> (f A) B cause there you can't apply from right to left as the operation (f A) bug everything

ReplyDeleteI've been looking for a good explanation of lambda calc type inferencing (with worked-through examples) for hours, and this is the first source I've found that has been helpful. Thanks so much! :)

ReplyDeleteAlso found it very useful and easy to understand. thank you!

ReplyDelete