Abstract: Lambda calculus is the kernel of a universal programming language. It appears in an untyped version (cf. Lisp) and several typed versions (cf ML, Clean, Haskell). The simple types are freely generated from basic types by the function space operator that transforms types A, B into A->B. This innocent looking data set (of types) has powerful consequences. Next to the freely generated types one also can 'fold' them to satisfy equations, obtaining the recursive types (first employed in Algol-68). After that one can impose a partial order on types. Finally, one can use intersections (greatest lower bounds) on these partial orders. Having arrived here one is able to describe all untyped terms, but now with a natural classification system.
Abstract: Lambda calculus is the kernel of a universal programming language. It appears in an untyped version (cf. Lisp) and several typed versions (cf ML, Clean, Haskell). The simple types are freely generated from basic types by the function space operator that transforms types A, B into A->B. This innocent looking data set (of types) has powerful consequences. Next to the freely generated types one also can 'fold' them to satisfy equations, obtaining the recursive types (first employed in Algol-68). After that one can impose a partial order on types. Finally, one can use intersections (greatest lower bounds) on these partial orders. Having arrived here one is able to describe all untyped terms, but now with a natural classification system.