Constraining Complexity in the Generics Design
summary
Allowing interfaces-with-methods inside union constraints makes the compiler’s implication check coNP-hard by reduction from Boolean satisfiability: the construction maps each Boolean variable to two interfaces (X and notX), adds “at least one” and “both” interfaces, and asks if formula∧atLeastOne implies notBoth. That makes precise checking potentially exponential and exploitable (C++ has similar cases). Practical compromises are one-level unions (DNF-like restriction), a conservative checker that rejects when unsure, or timeouts.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:40Union elements
- 2:37P vs NP
- 4:40NP Hard
- 6:22Co NP Hard
- 8:57Reduction Proof
- 11:07Solution
- 12:36Proof
- 14:18Frustration
- 14:48Ignore the problem
- 16:08Subproblems
- 18:09Type Checker
- 21:04Type Switches
- 23:08Conclusion
related talks
30mConstraint Typing with Boolean Algebra
29mGenerics Unconstrained!
16mPolymorphic Types and Effects with Boolean Unification
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)
01h 04mKnowledge Compilation for Quantification and Synthesis
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
33mSolving constraints during type inference