Function Application

So we now have a generic function that can return anything that it is passed. But we have not yet seen how to pass it anything. Since we have a generic function like this, the first thing we need to do is type-constrain it. This means we must tell it what that α is in ∀ α.α→α. We do this using type application syntax. Let's see what this looks like in practice. (LAMBDA a.lambda x:a.x) [forall b.b->b] Here we have constrained the type to be the same as its inner function. This means that we now have a function whose input is the identity function, and whose output is the same identity function. Talk about functional.

If you're confused at this point, think about it this way. Imagine playing catch with friend. Whatever you pass them, they'll immediately pass back to you. However, they don't want to be caught off guard, so before you pass them anything you have to call out what it is you're passing: "Ball", "Soda", "Large Tractor Trailer"! We're doing the same thing with our function. It will return anything that we give it, as long as it first knows what that is. In this case, we're telling it that we want to give it a function identical to itself. Now let's try that. (LAMBDA a.lambda x:a.x) [forall b.b->b] (LAMBDA b.lambda y:b.y) Now that we've given it a function of type ∀ α.α→α, our final output is just that function which was handed back to us. It might not be very exciting, but we've finally written a program that actually does something. Now let's see how to make it do something useful.