• Recursive types, generics, and subtyping: Essential for modern programming languages. Recursive types describe unbounded data, generics define parametrized data by abstracting concrete types, and subtyping enables specific types to be treated as general supertypes for code reuse. Structural subtyping is flexible.
• Challenges and proposed solution: The combination of these features is hard to manage. Structural subtyping with recursive types and generics is undecidable. In the POPL 2024 paper and its implementation, a reconstruction of the interaction is proposed.
• Parametric subtyping: Establishes when type constructors are parametric. It adapts Reynolds's characterization for type constructors. Examples include subtyping rules for stack, pushes, and pops.
• Deciding structural subtyping for monomorphic types: Using a saturation-based decision procedure with examples of even and odd natural numbers to prove subtyping.
• Deciding parametric subtyping: In the presence of generics, saturation is not guaranteed. Parametric subtyping is a fragment of structural subtyping that is decidable. The decision procedure has two phases: forward inference and backward construction.
• Further details and comparison: For more details, refer to the POPL 2024 paper and the online repository. Parametric subtyping is more flexible than Java and Scala's nominal subtyping. Scala has additional features like duck typing and variance annotations that parametric subtyping doesn't cover.
• Authors and disclaimer: Henry DeYoung, Andreia Mordido, Frank Pfenning, and Ankush Das contributed. The blog posts represent personal views and do not represent ACM SIGPLAN.