{"id":"8c0360a3-60e2-40f6-a9d2-ca36ba4a78cb","arxiv_id":"2603.23360","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A conservative extension of System F<: with Dom/Range projection types type-checks applications through abstract function types soundly, without unsafe any.","lead":"F<:DR adds domain and range projection types to System F<:, letting a function of unknown type F be applied to an argument of type Dom(F) and return Range(F) without exposing F as an arrow type. The authors prove soundness and normalization by logical relations and argue this safely generalizes TypeScript's Parameters/ReturnType idiom.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The t-app-dr rule is sound only if LF holds for all value interpretations (Lemma 5.3), but the proof is sketched, the LF definition has a variable-binding typo, and the promised Rocq artifact is absent.","rationale":"The central claim is that t-app-dr is semantically sound and weakly normalizing. That claim rests on the LF invariant and on Lemma 5.3, which asserts LF for every type interpretation. The reader identified exactly this as the weakest assumption, and I agree: the proof is a one-line sketch, the Dom/Range cases are nontrivial, and the printed LF definition contains a binding typo. However, my own analysis suggests the lemma may well be provable via a path-shifting argument, so I do not see a demonstrated unsoundness. The paper explicitly claims a Rocq mechanization but does not include the artifact, so the correctness of the central rule is currently an unverified claim rather than a checked theorem. The appropriate verdict remains CONDITIONAL -- the condition being a complete, compilable mechanization and a corrected LF definition. Since this does not move the reader's conditional verdict, I recommend UNCHANGED.","tokens_in":21943,"tokens_out":34152,"duration_ms":349085,"concrete_test":"Obtain the Rocq development and check: (1) the LF definition in Fig. 7 binds the lambda parameter (x), not the closure variable (v); (2) Lemma 5.3 is proved for T = Dom(U) and T = Range(U) by instantiating LF(VJUK) at the shifted path s.dom / s.ran and does not rely on an unstated assumption. If the artifact is unavailable or the proof term fails, the soundness of t-app-dr is unsubstantiated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"F<:DR's central rule (t-app-dr) is justified semantically by the LF invariant: if VJFK contains a value and VJFK^{.dom} contains an argument, the value must be a lambda-abstraction whose application lands in VJFK^{.ran}. The fundamental theorem (Thm 5.6) needs LF for every VJTK; this is Lemma 5.3, whose entire proof is 'By induction on type T'. The Dom/Range cases require shifting the selection path (s -> s.dom / s.ran) and a nested path/positivity argument that the paper does not give. More concretely, the displayed LF in Fig. 7 evaluates the body as ⟨(H,(v,v1)), t⟩, but the closure is ⟨H, λx.t⟩ — the parameter should be x, not the closure metavariable v. As printed, the invariant is not the right statement. The paper claims Rocq mechanization but supplies no artifact, so the central soundness claim is not independently checkable. This is a verification gap, not a demonstrated counterexample.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":22267,"tokens_out":7215,"duration_ms":73713,"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":[{"comment":"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.","section":"Section 5.4.1, Figure 7 (LF definition)"},{"comment":"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.","section":"Lemma 5.3, Section 5.5"},{"comment":"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.","section":"Abstract, §1, §5.5, §6.4 (Rocq artifact)"},{"comment":"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.","section":"Section 5.4.3 / Figure 8 / Theorem 5.6"}],"minor_comments":[{"comment":"The proof says 'Derived from semantic subtyping lemma (Theorem 5.4)', but the referenced statement is Lemma 5.4, not a theorem.","section":"Section 5.5, proof of Theorem 5.5"},{"comment":"The label '(f-snd-std)' should be '(t-snd-std)' for consistency with the other typing rules.","section":"Figure 9"},{"comment":"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.","section":"Figure 7, LF notation"},{"comment":"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.","section":"Figure 8 and §5.4.2"},{"comment":"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.","section":"§4.1, Figure 1"}],"recommendation":"major_revision","confidential_remarks":"The core idea is appealing and the proof strategy is plausible, but the binding error in LF and the absence of the promised Rocq artifact are serious. I would make the artifact and a complete proof of Lemma 5.3 conditions of acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is a real idea: F<:DR closes a gap in System F<:, letting you type f(x) from f:F and x:Dom(F) without exposing the arrow type. That is genuinely new compared to TypeScript's unsound Parameters/ReturnType and DOT's selectors. The subtyping rules for Dom/Range are clean, the eta-expansion motivation is right, and the pair extension shows the path-selection technique generalizes. I would not call it a paradigm shift; it is a solid within-subfield contribution that deserves a serious referee.\n\nThe weak spot is exactly where the reader puts it. The whole system rests on the LF invariant: if a value interpretation has an inhabited domain, the value must be a lambda and application lands in the range. If that fails, t-app-dr breaks. But Lemma 5.3's proof is one line ('By induction on type T'), which hides the hard cases: type variables, positivity, and the prepended selectors. More concretely, the LF definition in Figure 7 binds the closure environment with (H,(v,v1)) where it must be (H,(x,v1)); the printed statement is not the right one. That is a typo, but it sits inside the proof's key definition.\n\nThe bigger problem is the missing Rocq artifact. The abstract and intro say the system is mechanized; the paper does not provide a link, a repository, or any evidence beyond the claim. Without that, the central soundness assertion is not independently checkable. This is a verification gap, not a demonstrated counterexample, so I would not call the paper unsound; I would call it unverified.\n\nThe paper also spends a lot of space on expository motivation (e.g., Section 3), which is fine but compressible.\n\nRecommendation: send to peer review. The idea is solid and new; the authors must supply the artifact and repair the LF definition before acceptance. As it stands, I would not cite the soundness result in my own work until the machine-checked proof is available, but I would happily read a revised version and would bring this to a reading group to discuss the rule and the invariant.","headline":"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.","tokens_in":22679,"tokens_out":2711,"would_cite":false,"duration_ms":25561,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B40","68N18"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["domain types","range types","subtyping","parametric polymorphism","System F<:","logical relations","type projections","weak normalization"],"falsifier":"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","tokens_in":21839,"feed_emoji":"🎯","tokens_out":5685,"duration_ms":51731,"temperature":0.7,"pith_summary":"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<T>/ReturnType<T> idiom, which currently leans on the unsafe any type.","feed_headline":"Abstract function types can now be called safely","feed_subtitle":"Typing f(x) from f:F and x:Dom(F) gives precise results, no unsafe any bound","key_machinery":"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","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Call any F with a Dom(F) value: precise and safe","Forget forall: Dom(F) proves F is callable","Domain and range projections: call without quantifiers","Sound and normalizing: type calls with Dom/Range","Precise calls without quantifiers: use Dom and Range"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Call any F with a Dom(F) value: precise and safe","Forget forall: Dom(F) proves F is callable","Domain and range projections: call without quantifiers","Sound and normalizing: type calls with Dom/Range","Precise calls without quantifiers: use Dom and Range"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000963,"raw_usage":{"total_tokens":4004,"prompt_tokens":881,"completion_tokens":3123,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":625,"completion_tokens_details":{"reasoning_tokens":3039}},"tokens_in":625,"tokens_out":3123,"duration_ms":23601,"temperature":1.0,"reasoning_tokens":3039,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T17:32:45.999147+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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","supporting_citations":[],"review_version":1}