Abstract

Programming With Intersection Types, Union Types and Polymorphism written By Benjamin C. Pierce on 1991 is reviewed. This technical report shows a polymorphic lambda-calculus with intersection and union types. The system is quite theoretical, and lacks the ability to introduce record-like intersection types; but one can define intersection function types. Finitary polymorphism is employed in the system, while a more advanced “for” construct is introduced to make it even more powerful. An encoding of union types using intersection types are introduced by the paper. Finally, I will show some comparisons between this system and other practical languages.