Higher-order algebra with transfinite types

We extend the simple type system of higher-order algebra with transfinite types. We present a general model theory for transfinite higher-order algebra including results on the existence and construction of free and initial models, and a sound and complete equational calculus. We demonstrate the use of transfinite types for modelling polymorphism by specifying a simple polymorphic functional programming language.