One facet of polymorphism (wrt the Lambda Calculus) is the study of functions that take polymorphic arguments i.e., the action in the body of the function does not depend on the type of the arguments.

First, some notation. We denote a function that takes some argument x of type t and returns e of type s as \x:t.e:s. We say this function has type t->s. To apply a function to an argument, we just use juxtaposition: (\x:t.e:s) v. Note that v:t and the whole expression has type s.

So what functions are of type t->t? Since we know nothing about the type t, the only thing we can return is the argument itself: \x:t.x:t. This is not very interesting.

What about functions of type t->t->t? Basically, we take two arguments (this is a curried function), and since we know nothing about the type (i.e., we can't add the arguments or whatever), all we can do is return the first argument (T = \x:t.\y:t.x) or the second (F = \x:t.\y:t.y). So what type is this really (t->t->t)? Well, it's bool, the type with only two elements. Note that I called these elements T and F.

Now let's have some fun with this new way of looking at bool. We can make an if-then-else statement simply by function application: b e1 e2 evaluates to e1 if b = T and to e2 if b = F. Thus e1 is the then clause and e2 is the else clause. We can construct the function NOT = \b:bool.b F T and AND = \x:bool.\y:bool. x y F.

What about functions of type t->(t->t)->t? Consider \z:t.\s:t->t.e:t. Well, we take as arguments z:t and a function s:t->t. Since we need to return something of type t, we can just return z. Or we can return s z, or s (s z) or s (s (s z)), etc. So what type is this? You guessed it, it's nat, the natural numbers (z is zero, and s is the successor function. We can have a lot of fun with this one, but that is beyond the scope of this writeup. Take a course in lambda calculus or type theory if you want more.

Does your head hurt yet?