Type systems, especially when used in programming languages, often benefit from having a notion of intersection amongst their primitive operators.
Thus, we can postulate a binary operator on types, along with an introduction rule
That is: if has both type and , then it can be typed by their intersection.
Conversely, we can eliminate the intersection by 'forgetting' it:
Such type systems have many uses:
Bono, Viviana, and Mariangiola Dezani-Ciancaglini. 2020. ‘A Tale of Intersection Types’. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 7–20. Saarbrücken Germany: ACM. https://doi.org/10.1145/3373718.3394733.
@inproceedings{bono_2020,
address = {Saarbrücken Germany},
title = {A tale of intersection types},
doi = {10.1145/3373718.3394733},
booktitle = {Proceedings of the 35th {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {ACM},
author = {Bono, Viviana and Dezani-Ciancaglini, Mariangiola},
month = jul,
year = {2020},
pages = {7--20}
}