Set-theoretic types for polymorphic variants

2016/06/03 by Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyen +1 · 1 voice
Computer Science · #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Software Engineering Research #cs.PL

paper · pdf · doi:10.1145/2951913.2951928

openalex publication_date 2016/08/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30

Abstract

Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system whose behaviour is in some cases unintuitive and/or unduly restrictive.

Citations

• Semantic subtyping

Discussions

• Set-Theoretic Types for Polymorphic Variants [lobsters, 4 points, 0 comments]

Related

• Phantom Types and Subtyping
• Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
• Polymorphic Records for Dynamic Languages
• Generic Programming with Combinators and Objects
• Programming with Union, Intersection, and Negation Types