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.

翻译：诸如Python和JavaScript等动态语言广泛使用函数装饰器来扩展行为。在TypeScript中，对此类模式进行类型标注的常见做法涉及 Parameters<T> 与 ReturnType<T>。实践中，这一惯用法依赖于一个用不安全类型 any 表达的函数类型约束 T，从而削弱了静态保证。其核心是一个标准类型化原则：仅当被调用者暴露为箭头类型时，应用才具有合法性。我们提出 F<:DR 演算，为任意类型 T 添加定义域（Dom(T)）与值域（Range(T)）投影类型。这些投影允许通过抽象函数类型对应用进行类型化：类型为 Dom(T) 的实参证明了可调用性，而结果则被类型化为 Range(T)。该设计并非替代而是在 System F<: 中通过子类型化保持标准箭头型应用的可容许性。我们在Rocq中对 F<:DR 进行机械化，并利用带路径选择的逻辑关系证明语义类型安全性——这种路径选择延迟了投影解释，直到函数结构被解析。相同技术可扩展至其他投影类型，例如针对原始对（即积类型）的投影。