And what is more? We moved at a high order, but then we may even want to have types depending on terms. We had so far terms depending on terms, just first order applications. We had terms depending on types like in second order calculus. We had types depending on types like in the constructor calculus that I showed before. Then we may ask: why not types depending on terms? Well, if we follow this idea, the result is a formal system that is called LF (Logical Frameworks) and we cannot describe it certainly here in detail. However, the informal example about these types depending on terms is quite simple. If we take a natural number n, then for any n, An - that is n copies of A - is certainly a proposition, and it is also a proposition An -> B. We may think that Pn.An -> B is the type of all the functions that, for any n, return a function An -> B. Now, this notion is called a dependent type and it is embodied in this calculus that is called LF.

---