However, sometimes we do not want all the freedom of type-free l-calculus. For instance, it is very handy to have in programming languages a type checker that allows to check at compile time several errors, several programming mistakes. And this is what is usually done also in functional programming languages. For instance, we will see in the following lectures that in Standard ML that there are many types. Any term gets a type. And, for instance, it is certainly forbidden to apply a function to itself. So, the function that takes a variable x and applies x to itself is certainly forbidden. And so, we want to add types to our formal system. As a result, we get a different formal system, that we call typed l-calculus. Since in this system we just have variables, functional abstraction, and functional application, it is quite natural to have also a very simple type structure. Our type structure only consists of base types and function types. These function types correspond to function abstractions. Now, in the slides we have the type inference rules for our system. The rule on the left is the one for functional application. You see that it corresponds to the fact that we have a function from A to B and an argument of type A. Then of course the result of applying the function M to the argument N is of type B. On the other hand, the rule on the right is the one for functional abstraction. If we are able to deduce that M is a result in type B whenever we assume that the variable x is in type A, then the function that takes x as an argument and gives us back M is a function from A to B. And this is all the typed l calculus. These are all the rules for this simple formal system.

---