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

TL;DR

This paper introduces F<:DR, a calculus with domain and range projection types for better static typing of functions in dynamic languages, improving type safety without sacrificing flexibility.

Contribution

It proposes a novel calculus adding domain and range projections, enabling precise typing of function applications in a way that complements standard arrow types.

Findings

Mechanized in Rocq and proven soundness using logical relations.

Supports typing of primitive pairs with extended projections.

Enhances static guarantees in dynamic language patterns.

Abstract

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.