Basic polymorphic typechecking (Q580956)

``Polymorphic'' means to have ``many forms''. As related to programming languages, it refers to data or programs which have many types, or which operate on many types. In this paper we discuss Milner's polymorphic typechecking algorithm, which has proved very successful: it is sound, efficient, and supports a very rich and flexible type system. It was initially developed for the ML language, and has since been adopted by many other languages. One unique feature of Milner's algorithm is its ability to infer types in the absence of type declarations. This comes for free: in the attempt to deal with programs which can be reused on many types, the algorithm searches for the best (most abstract) type of a program. Such best type is independent of type declarations, which can only be used to reduce the generality of the most abstract type. The pragmatics of polymorphic typechecking has so far been restricted to a small group of people. In the hope of making the algorithm more widely accessible, we also include an implementation in the form of a Modula-2 program. Although clarity has sometimes been preferred to efficiency, this implementation is reasonably efficient and quite usable in practice for typechecking large programs.