Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types

Abstract

Subtyping allows polymorphism at a low price: a concise type such as Int -> Top covers every function that accepts an integer, whatever it returns, whereas the parametric alternative $\forall$ B.Int -> B spends a quantifier and a type parameter, a difference that compounds as types nest and leaves signatures heavyweight and less intuitive. The polymorphism via subtyping, however, is not always enough, as upcasting to Int -> Top forgets the result type, so a program that needs the precise result must abandon the concise signature and return to full parameterization. The missing middle ground is a lightweight polymorphism that keeps the concise, readable types of subtyping yet recovers the precision of parametricity. TypeScript's Parameters<T> and ReturnType<T> reach for it but stand only on the unsafe any, and type destructors reach it soundly but only for covariant types, leaving the arrow-type case open. We present F<:DR, a conservative 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.