| layout | post |
|---|---|
| title | A more theoretical view of Intersection/Union Types |
| authors | Jimmy |
| date | 2016-11-18 10:30:00 +0800 |
| venue | CB 313 |
| categories | Jimmy 2016 |
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.