Implementing Set-Theoretic Types

Title:

Implementing Set-Theoretic Types

Authors:

M. Laurent, K. Nguyễn

Publication:

Proceedings of the ACM on Programming Languages 10 (OOPSLA2)

DOI:

Year:

2026

Link:

Abstract:

Set-theoretic types provide a rich type algebra that supports unrestricted unions, intersections, and negations, together with a decidable type constraint-solving algorithm known as tallying. These types are particularly well suited for typing dynamic languages, where functions often exhibit both generic and overloaded behavior. However, the complexity of their implementation has hindered their widespread adoption. In this paper, we introduce a modular representation for set-theoretic types and revisit the algorithms for subtyping and tallying. We compare our approach with the historical CDuce implementation and evaluate the performance impact of some optimizations and design choices.

BibTeX:

@article{laurent_implementing_2026,
    title = {{Implementing Set-Theoretic Types}},
    author = {Laurent, Mickaël and Nguyễn, Kim},
    year = {2026},
    journal = {{Proceedings of the ACM on Programming Languages}},
    number = {OOPSLA2},
    doi = {10.1145/3839466},
    pages = {334:544--334:570},
    url = {https://dl.acm.org/doi/10.1145/3839466},
    volume = {10},
}