Pith. sign in

REVIEW 4 major objections 5 minor 3 references

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

T0 review · 4 major / 5 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A type system can type f(x) from f:F and x:Dom(F), letting abstract function types be called while preserving the result type.

desk verdict A genuinely new typing mechanism with a plausible soundness story, but the load-bearing invariant is sketched, the mechanization is absent, and there is a binding typo in the LF definition. read the letter →

arxiv 2603.23360 v2 pith:TPYJISMC submitted 2026-03-24 cs.PL

Siyuan He , Songlin Jia , Tiark Rompf This is my paper
classification cs.PL MSC 03B4068N18
keywords domaintypesrangesubtypingparametricpolymorphismSystemF<:logicalrelationstypeprojectionsweaknormalization
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper introduces F<:^DR, a conservative extension of System F<: with domain and range projection types Dom(T) and Range(T), and a single application rule: a well-typed argument of type Dom(F) is itself the witness that F is callable, so f(x) receives type Range(F) for arbitrary F. This gives safe, lightweight parametric polymorphism: a function type variable needs only the trivial bound Top, yet applications through it remain precisely typed, closing the gap between subtyping-based polymorphism and full parametric polymorphism. The authors prove semantic type soundness and weak normalization by logical relations, using a path-selection technique that delays the interpretation of a projection until the underlying arrow structure is resolved. If right, this supplies a sound foundation for TypeScript's Parameters/ReturnType idiom, which currently leans on the unsafe any type.

What carries the argument

The central object is the pair of type projections Dom(T) and Range(T), governed by introduction/elimination subtyping rules that make Dom(𝐴→𝐡) equivalent to A and Range(𝐴→𝐡) equivalent to B, with contravariant and covariant congruence respectively. The argument-carrying work is done by the typing rule (t-app-dr), which replaces structural inspection of the callee type with a domain-typed argument that witnesses callability. The logical-relations proof is carried by path selection: selection paths (dom, ran) are appended to value interpretations, and the interpretation of a projection defers to the interpretation of the underlying type, resolving once an arrow type is reached; the predicate

What would settle it

Construct a closed type T and a closed term t : Dom(T) such that the big-step normal form of t is not a λ-abstraction (or, equivalently, find a value interpretation V with LF(V) false in a context satisfying the environment interpretation). The paper's Lemma 5.3 claims this is impossible; exhibiting one would refute Corollary 5.7. A computational check: implement the logical relations directly (or inspect the supplied proof artifact) and search for a type T where the syntactic subtyping rules derive Dom(T) inhabited but no arrow subtype T <: A→B is derivable; if found, the proof sketch's 'by i

Watch

Extended reading notes

Core claim

The central claim is that the rule (t-app-dr) β€” from f:F and a term x:Dom(F), derive f(x):Range(F) β€” is sound and weakly normalizing for the whole calculus. Soundness rests on the invariant that Dom(T) is inhabited only when T is, or is a subtype of, an arrow type, so passing a value of type Dom(F) is genuine evidence that F is callable. The logical-relations model handles projections by carrying selection paths (dom, ran) on values and resolving them only when the underlying type is exposed as an arrow type; the well-formed-functionality predicate LF(V) records that every value interpretation behaves like functions when its domain is inhabited. Standard arrow application remains admissible

Load-bearing premise

The entire result rests on the invariant that Dom(T) has an inhabitant only when T behaves like an arrow type, so the argument of type Dom(F) is a genuine witness that F is callable; if any type with an inhabited domain projection were not a subtype of an arrow type, the application rule would be unsound.

Editorial extensions

If this is right

  • TypeScript's Parameters<T> and ReturnType<T> idiom can be given a sound typing rule that does not rely on the any type; the result type of an abstract callee is exactly Range(F), not any.
  • A function type variable needs no informative bound (only <: Top) for its applications to type precisely, so polymorphic wrappers and Ξ·-expansions become lighter-weight than bounded-quantification encodings.
  • The standard application rule remains derivable through subtyping, so adding domain/range types does not break existing System F<: programs.
  • The path-selection technique generalizes to other projection operators, demonstrated with first/second projections on pair types, suggesting a uniform approach to projection-based typing.
  • The paper's Corollary 5.7 gives a concrete guarantee: every well-typed closed term reduces to a value in the semantic interpretation of its type, i.e., progress and weak normalization hold together.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the LF invariant holds, the calculus can be viewed as a type-level reflection of 'callability': a function type is not a kind of type, but a property witnessed by arguments. That could be pushed further to sum types, records, or lists with projectors, exactly as the paper sketches.
  • The authors leave implicit the possibility of combining domain/range types with a typeof term-level operator; that would complete the analogy to ReturnType<typeof f> and make the calculus directly usable for term-level dependent-looking idioms.
  • A natural test of the design: whether the projection rules can be made definitional (reduction/equality) rather than only subtyping, which might affect decidability or principal types; the paper does not address this.
  • The semantic soundness proof with path selection suggests a relational reading of Dom(T) as a 'domain set' in a set-theoretic model; if carried further, this could yield free theorems or parametricity statements for F<:^DR.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper introduces F<:^DR, a conservative extension of System F<: with first-class domain and range projection types Dom(T) and Range(T). The central typing rule (t-app-dr) types an application f t as Range(F) from f : F and t : Dom(F), deferring the need for F to be syntactically exposed as an arrow type; the paper argues that an inhabited Dom(F) witnesses that F behaves like a function type. The metatheory is developed via logical relations with a 'selection path' technique that delays the interpretation of projections until the underlying arrow type is resolved. The authors claim semantic type soundness and weak normalization (Corollary 5.7 via Theorems 5.5 and 5.6), and extend the same mechanism to product types and Fst/Snd projections. The paper also states that the development is fully mechanized in Rocq, but no artifact is provided.

Significance. If the metatheory is correct, the paper offers a genuinely useful middle ground between subtyping-only and full parametric polymorphism: abstract function types can be applied precisely without informative bounds, and standard arrow application remains admissible by subtyping. The selection-path technique is a plausible and potentially reusable way to handle type operators that need to be resolved by structural information. The extension to pairs suggests that the approach generalizes beyond arrow types. The paper's main weakness is that the central semantic invariant (LF) is presented with a variable-binding error, the key lemma establishing it is only sketched, and the claimed Rocq artifact is absent. These issues make the soundness claim not independently checkable as submitted, so the significance is conditional on a complete and corrected proof.

major comments (4)
  1. [Section 5.4.1, Figure 7 (LF definition)] The displayed well-formed-functionality predicate LF(V) is not well formed as printed. The function value is a closure ⟨H, Ξ»x.t⟩, so the body must be evaluated in the environment extended by the bound variable x, i.e. ⟨(H,(x,v1)), t⟩. The manuscript instead writes ⟨(H,(v,v1)), t⟩, extending the environment with the value metavariable v, which is not a term variable. This is not a mere notation nit: Lemma 5.3 is supposed to show LF(VJ𝑇Kρ) for every type T, and LF is exactly the invariant that makes t-app-dr sound. As printed, the lemma's statement is not the right one.
  2. [Lemma 5.3, Section 5.5] The proof of Lemma 5.3 is only 'By induction on type T...' with a sentence saying that other cases follow because LF(T) is general for any selection paths. The load-bearing cases are Dom(T) and Range(T), where the interpretation shifts the selection path (VJDom(T)Kρ^s = VJTKρ^{s.dom}); the induction hypothesis must be applied at a different path, and one must maintain the path-positivity invariant. The text supplies none of this argument. Since Lemma 5.3 is the key semantic justification for the application rule and for type instantiation in the βˆ€-case, this is a verification gap in the central soundness claim.
  3. [Abstract, Β§1, Β§5.5, Β§6.4 (Rocq artifact)] The paper repeatedly claims that the system is 'fully mechanized in Rocq' and refers readers to 'our artifact' for the complete proofs, but no artifact, repository URL, or proof-script listing is provided anywhere in the manuscript. Given that the paper's metatheory is presented as a series of sketches ('By induction on ... β–‘'), the machine-checked proof is not merely an ancillary convenience but an essential component of the verification. Without it, the central soundness result is not independently checkable.
  4. [Section 5.4.3 / Figure 8 / Theorem 5.6] Figure 8 presents only 'selected' semantic typing rules and the surrounding text says the full presentation is omitted. Theorem 5.6 is then proved by induction on the syntactic typing relation. An induction over all typing rules requires the semantic counterparts of every rule, including t-abs, t-tabs, t-tapp, and the product rules, to be stated. As submitted, the fundamental theorem's proof is not self-contained even modulo the artifact issue.
minor comments (5)
  1. [Section 5.5, proof of Theorem 5.5] The proof says 'Derived from semantic subtyping lemma (Theorem 5.4)', but the referenced statement is Lemma 5.4, not a theorem.
  2. [Figure 9] The label '(f-snd-std)' should be '(t-snd-std)' for consistency with the other typing rules.
  3. [Figure 7, LF notation] The notation s[‒↦→‒.dom] is used but never formally defined. The text explains that the selectors are 'prepended', but replacing the root of the path is not the same operation as prepending in general; a precise definition of path replacement is needed.
  4. [Figure 8 and Β§5.4.2] The notation VJ𝑇Kρ is used without a selection path, while Figure 6 defines VJ𝑇Kρ^s. A convention that the missing path is the root β€’ would remove ambiguity.
  5. [Β§4.1, Figure 1] The grammar lists 'Function Variables' separately from ordinary variables, but the typing rules do not distinguish them. This extra category is unnecessary and can confuse the reader.

Circularity Check

0 steps flagged Β· score 0.0 of 10

No significant circularity: the soundness of t-app-dr is discharged by a logical-relations argument, not by assuming the rule or by fitting; self-citations are proof-technique borrowings.

full rationale

The central derivation chain is self-contained relative to the paper's own definitions. The application rule t-app-dr (Fig. 3) is not assumed as a semantic axiom: it is interpreted as st-appdr (Fig. 8), and its soundness is delegated to the well-formed-functionality invariant LF (Fig. 7) and Lemma 5.3, which claims LF(VJTK) for every value interpretation by induction on T. This is a standard logical-relations argument; even though Lemma 5.3 is only sketched ('By induction on type T'), the arrow, base, Top/Bot, Dom/Range, and quantifier cases have semantic clauses (Fig. 6) that are not definitionally identical to the typing rule. No parameter is fitted to data and no 'prediction' is statistically forced. The paper's citations to earlier work by the same group (Amin & Rompf 2017; Wang & Rompf 2017; Rompf & Amin 2016) supply the big-step-semantics and selector techniques; they are used as proof infrastructure, and the paper explicitly distinguishes its use of selectors ('similar in technique, the core ideas are different'). They do not assume the target theorem or rule out alternatives, so this is not load-bearing self-citation. The main legitimate concerns are verification gaps rather than circularity: the promised Rocq artifact is not provided (abstract says 'All are mechanized in Rocq', but §5.5 only says 'refer interested readers to our artifact for details'), and the printed LF clause in Fig. 7 evaluates the body as ⟨(H,(v,v1)), t⟩, which appears to bind the lambda variable to the function value rather than the argument. These issues affect confidence in the proof, not the circularity score.

Assumptions & free parameters 0 free parameters Β· 3 assumptions Β· 3 invented entities

The calculus itself is the contribution; there are no fitted empirical parameters. The axioms are the subtyping rules for Dom/Range, the path-selection semantic model, and the LF/LP invariants. These design choices are not independently evidenced beyond the claimed mechanization.

assumptions (3)
  • standard math Underlying System F<: subtyping/typing and big-step operational semantics are standard and taken as background.
    Sections 4.1-4.3 build on F<:; the logical-relations framework of Amin and Rompf 2017 is used as infrastructure.
  • domain assumption Every well-formed value interpretation V in the environment satisfies LF(V) and LP(V); this invariant is imposed on type-variable instantiations.
    GJΞ“K in Figure 7 requires LF/LP for bound type variables; Lemma 5.3 claims it holds for all syntactic types, but the proof is a sketch.
  • ad hoc to paper Selection-path semantics: Dom(T) and Range(T) are interpreted by appending dom/ran selectors, and arrow types resolve these selectors to their components; non-arrow types under positive/negative non-root paths collapse to Top/Bot.
    This is the paper's chosen semantic model for projections. It is not forced by external evidence, and its adequacy is exactly what the unavailable Rocq proof would establish.
invented entities (3)
  • Dom(T) / Range(T) projection types
    purpose: Allow typing f(x) without exposing F as an arrow type
    New type constructors with subtyping rules; no empirical handle beyond the internal formalization.
  • Selection paths and dom/ran selectors
    purpose: Delay interpretation of projections in the logical relation until arrow structure resolves
    Proof-technique device; no independent falsifiable predictions.
  • LF/LP well-formedness invariants
    purpose: Guarantee that inhabited domain/range or pair projections imply function/pair behavior
    Internal semantic invariants introduced to make the fundamental theorem go through.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types." pith.science (2026). https://pith.science/paper/TPYJISMC

@misc{pith2026260323360,
  author       = {Pith},
  title        = {Pith review of: Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TPYJISMC}},
  note         = {Machine review of arXiv:2603.23360}
}
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.

Figures

Figures reproduced from arXiv: 2603.23360 by the authors.

Figure 1
Figure 1. The syntax of F 𝐷𝑅 <: calculus. Subtyping Ξ“ ⊒ 𝑇 <: 𝑇 Ξ“ ⊒ 𝑇 <: Top (s-top) Ξ“ ⊒ Bot <: 𝑇 (s-bot) Ξ“ ⊒ 𝑇 <: 𝑇 (s-refl) 𝑋 <: 𝑇 ∈ Ξ“ Ξ“ ⊒ 𝑋 <: 𝑇 (s-var) Ξ“ ⊒ 𝑇1 <: 𝑇2 Ξ“ ⊒ 𝑇2 <: 𝑇3 Ξ“ ⊒ 𝑇1 <: 𝑇3 (s-trans) Ξ“ ⊒ 𝑇1 <: 𝑆1 Ξ“ ⊒ 𝑆2 <: 𝑇2 Ξ“ ⊒ 𝑆1 β†’ 𝑆2 <: 𝑇1 β†’ 𝑇2 (s-fun) Ξ“, 𝑋 <: π‘ˆ ⊒ 𝑆 <: 𝑇 Ξ“ ⊒ βˆ€π‘‹ <: π‘ˆ . 𝑆 <: βˆ€π‘‹ <: π‘ˆ .𝑇 (s-all) Ξ“ ⊒ 𝑇1 <: Dom(𝑇1 β†’ 𝑇2) (s-dom-intro) Ξ“ ⊒ Range(𝑇1 β†’ 𝑇2) <: 𝑇2 (s-range-elim) Ξ“ ⊒ Dom(𝑇1 β†’ 𝑇2) <: 𝑇1 (s-dom-elim… view at source β†—
Figure 2
Figure 2. Subtyping rules of F 𝐷𝑅 <: calculus. 4.2 Static Subtyping [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source β†—
Figure 3
Figure 3. Typing rules of F 𝐷𝑅 <: 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. of type 𝑇1 β†’ 𝑇2 produces results of type at most 𝑇2, and thus its range type is upper bounded by 𝑇2. According to the function type variance (s-fun), the range type is covariant, so upcasting a function type results in a larger range type… view at source β†—
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: The syntax and path selection of the logical relations for [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]
Figure 5
Figure 5. Figure 5: Big-step Reduction of F 𝐷𝑅 <: -calculus. the selector dom projects the semantic interpretation of a function type to the interpretation of its domain type, while ran projects it to that of its range type. A selection path is written as a sequence (right appended) of se…
Figure 6
Figure 6. Figure 6: The definitions of value interpretations for [PITH_FULL_IMAGE:figures/full_fig_p015_6.png]
Figure 7
Figure 7. Figure 7: The environment and expression interpretation of the [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: The semantic subtyping and typing (selected) of the [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 9
Figure 9. Figure 9: The syntactic extensions for pairs from F 𝐷𝑅 <: calculus. The standard first (t-fst-std) and second rules (f-snd-std) are implied by (t-fst) and (t-snd) via subtyping on first and second types. 6 Case Studies: Projection Types for Pairs In Section 5, we have illustrate…
Figure 10
Figure 10. Figure 10: The big-step reductions and well-formedness for pairs from [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: The well-formedness, value interpretations, and updated environment types for pairs. [PITH_FULL_IMAGE:figures/full_fig_p020_11.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

3 extracted references

  1. [2]

    Microsoft

    Microsoft/Vscode. Microsoft. https://github.com/microsoft/vscode/blob/2a5a1757fd2a4d02a8fbb647a7a70a79c3e94ca0/ src/vs/editor/browser/viewParts/contentWidgets/contentWidgets.ts#L626

  2. [3]

    O’Reilly Media, Inc

    RocketChat/Rocket.Chat. Rocket.Chat. https://github.com/RocketChat/Rocket.Chat/blob/ ed12cc140ad541373f9e1a6d26d72c7c445c1de5/apps/meteor/app/settings/server/Middleware.ts Amal J. Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. InProgramming Languages and Systems, 15th European Symposium on Programming, ESOP 2006,...

    arXiv 2006

  3. [2026]

    Anomalyco/Opencode. Anomaly. https://github.com/anomalyco/opencode/blob/ f13da808ffb98bc0e582e227f3cf8f74d090b7d8/packages/opencode/src/util/rpc.ts#L46

Pith tools

Reviewed August 2, 2026 Β· model on record in the stance chip above.