Abstract

Types were invented by Russell to solve the logical paradoxes that resulted from Frege’s generalisaton of the notion of function. Since, the past 100 years saw new formalisations of the notions of functions and types that extend and put to better use Frege’s and Russell ’s inventions. Most such formalisations are extensions of Church’s simply typed λ-calculus. Currently, types and functions are the heart of logic and computation and not only are they so closely intertwined, but their evolution demands that they be treated in the same manner. Both are usually constructed, abstracted over and instantiated and the operations for abstraction, construction, instantiation and substitution act alike on both. This paper aims to give a framework where the relationship between functions and types takes into account the similarity of their construction, abstraction, instantiation and substitution. For such a “types as functions” framework to work, special forms of function abstraction need to be included