Subtyping provides polymorphism at a low cost: a concise type such as Int $\to$ Top covers every function that accepts an integer, whatever it returns, whereas the parametric alternative $\forall B.\,$ Int $\to$ B spends a quantifier and a type parameter to express the same. This cognitive overhead compounds as types nest. Subtyping, however, is not always enough: upcasting to Int $\to$ Top forgets the result type, so a program that needs the precise result must return to full parameterization. The missing middle ground is a lightweight form of polymorphism in the spirit of Hofmann and Pierce's type destructors and TypeScript's Parameters<T> and ReturnType<T>, which keeps the concise types of subtyping yet recovers the precision of parametricity. However, Hofmann and Pierce did not address contravariant positions such as function arguments, and TypeScript's utility types rely on the unsound `any` type. To address this gap, we present $F^{DR}_{<:}$, an extension of System $F_{<:}$ with first-class domain and range projection types, Dom(T) and Range(T), and an application rule that types f(x) from f : F and x : Dom(F) for an arbitrary type F. The demand that F be exposed as an arrow type is delayed from the definition site to the call site and discharged by the argument itself, as a value of type Dom(F) exists only when F is a subtype of an arrow type. A function type variable then needs no informative bound, only $<:$ Top, while its applications still type precisely, reaching the middle ground through a boundless quantification. We prove semantic type soundness and weak normalization by logical relations, where path selection delays a projection's interpretation until the underlying arrow type is resolved. The same machinery extends to product projections, which cooperate with domain and range in one system. All are mechanized in Rocq.

翻译：暂无翻译