Example

Now it's time to look at an example. Suppose we are given a term , where , and . Taking , , and , and we want to show that is typed to . How to do this? As before, we know the typing rules for -terms, so we can use algorithm to do typing derivation on that term, but the derivation tree turns out to be quite complicated. The first few steps of derivation are:

Now, to type , we must type and separately, and then do unification on type . Followings are the typing derivation for and , which you may not want to see the detail because of their complexity.

Let be typing environment . We have

>From our pre-obtained knowledge on , and , we know that . Now can be typed in this way:

By comparing the type of and , we can know that type must be , and thus the whole typing derivation is completed.

However, if we use subject reduction theorem, things become easy. We can do reduction on that long term first to get a much simpler term. Since reduction respects type, we can then type the new term to get a type for the original one. The typing becomes easier, because we totally avoid in typing or . First step is doing reduction.

Now typing is much easier: