Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
This work addresses a specific typing issue for developers using dynamic languages with static type systems, offering an incremental improvement over existing methods.
The paper tackles the problem of typing function decorators in dynamic languages like TypeScript, which currently rely on unsafe type 'any', by introducing a calculus F<:DR with domain and range projection types to provide stronger static guarantees. It mechanizes the calculus in Rocq, proves type soundness, and extends the technique to product types.
Dynamic languages such as Python and JavaScript widely use function decorators to extend behavior. In TypeScript, a common way to type such patterns uses Parameters<T> and ReturnType<T>. In practice, this idiom relies on a function-type bound for T that is expressed using the unsafe type any, which weakens static guarantees. At the core is a standard typing principle: application is justified only when the callee is exposed as an arrow type. We present F<:DR, a calculus that adds domain and range projection types, Dom(T) and Range(T), for arbitrary types T. These projections permit typing applications through abstract function types: an argument of type Dom(T) witnesses callability, and the result is typed as Range(T). This design complements, rather than replaces, standard arrow-based application, which remains admissible via subtyping in System F<:. We mechanize F<:DR in Rocq and prove semantic type soundness using logical relations with path selection, which delays projection interpretation until function structure is resolved. The same technique extends to additional projection types, illustrated for primitive pairs, i.e., product types.