Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Siyuan He, Songlin Jia, Tiark Rompf

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.

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

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.
Paper Structure (63 sections, 9 theorems, 14 equations, 11 figures, 1 table)

This paper contains 63 sections, 9 theorems, 14 equations, 11 figures, 1 table.

Table of Contents

  1. Introduction
  2. This Work.
  3. Scope.
  4. Informal Overview
  5. Revisiting Parameters and ReturnType in TypeScript
  6. Why Programmers Use Them
  7. Tracking Inferred Return Types.
  8. Abstracting over Platform-Specific Types.
  9. Composing with Other Type-Level Utilities.
  10. Any as the Escape Hatch.
  11. Revisiting Parametric Polymorphism
  12. Expressing Type Dependencies.
  13. Precision and Instantiation.
  14. Abstract Types and Structural Information.
  15. Takeaway.
  16. ...and 48 more sections

Key Result

lemma 1

If $\,X \notin T$, then for any value type environment $\rho$, and path ${\color{pathcolor!100}s}$, and value interpretation $V$, ${\mathbb{V} \llbracket {T} \rrbracket}^{\raisebox{0.1ex}{$\,{\color{pathcolor!100}s}$}}_{\rho} = {\mathbb{V} \llbracket {T} \rrbracket}^{\raisebox{0.1ex}{$\,{\color{pa

Figures (11)

  • Figure 1: The syntax of $\mathsf{F}^{DR}_{<:}$ calculus.
  • Figure 2: Subtyping rules of $\mathsf{F}^{DR}_{<:}$ calculus.
  • Figure 3: Typing rules of $\mathsf{F}^{DR}_{<:}$ calculus. The standard application rule t-app is implied by the domain and range application rule t-app-dr via subtyping on both domain and range types.
  • Figure 4: The syntax and path selection of the logical relations for $\mathsf{F}^{DR}_{<:}$ calculus.
  • Figure 5: Big-step Reduction of $\mathsf{F}^{DR}_{<:}$-calculus.
  • ...and 6 more figures

Theorems & Definitions (17)

  • lemma 1: semantic weakening
  • lemma 2: semantic substitution
  • proof
  • lemma 3: semantic functionality
  • proof
  • lemma 4: semantic subtyping
  • proof
  • theorem 1: fundamental of subtyping
  • proof
  • theorem 2: fundamental
  • ...and 7 more