When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-C...
summary
Introduces a declarative system F{≤} and an algorithm SuperF that uses multi‑bounded polymorphism to infer first‑class polymorphic types, encoding unions/intersections as upper and lower bounds. Implementation infers System F annotations, types the OCaml list module and prior literature examples without annotations, and uses a recursion‑avoiding heuristic that terminates by rejecting some valid programs (e.g. big Omega), so completeness is sacrificed for practicality while checking remains exponential in worst case.
AI-written summary · about