Pith. sign in

REVIEW 4 major objections 4 minor 1 cited by

A deterministic inference engine can beat the strongest published LLM prompt baseline on paired type-inference facts by separating the four sources of type evidence into monotone slots.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-01 12:00 UTC pith:G3UBYSKO

load-bearing objection Genuinely novel four-slot projection design with a plausible formal core, but the 513/513 benchmark headline is unauditable as presented. the 4 major comments →

arxiv 2607.19693 v3 pith:G3UBYSKO submitted 2026-07-22 cs.PL

Generic Constraints Projection: Four-Dimensional Type Inference for Dynamic Languages

Qunhui Zhang This is my paper
classification cs.PL
keywords type inferencedynamic languagesconstraint projectionstructural subtypingzero-annotation inferenceGenericablefluent chainsreceiver preservation
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper tries to show that the type information dynamic languages are often said to lack is recoverable without annotations, provided the four sources of evidence — assigned values, explicit declarations, contextual requirements, and structural operations — are kept in separate monotone slots on a stable definition-time template and combined only when a call is projected in a fresh session. Keeping the evidence separate avoids the spurious conflicts that arise when a single constraint set tries to equate values, requirements, and declarations. If the framework is right, a deterministic engine can recover exact types where classical gradual systems and LLM prompting have either plateaued or needed large models, and it can do so with formal convergence and conditional soundness guarantees. The paper reports 513/513 exact matches on paired ports of a 513-fact Python micro-benchmark, against 485/513 for the strongest published prompting baseline, with a statistically significant paired difference.

Core claim

The central claim is the stable-template/fresh-session decomposition: each unresolved parameter carries four constraint dimensions — value coverage (joined upward), a declaration anchor (single assignment), contextual requirements (met downward), and structural requirements (met downward) — and each call verifies its argument against a copy of the converged template, so repeated calls do not contaminate one another and return types specialize per call. Formalized over a finite-height structural preorder with an open type-matching relation, this yields monotonicity, local and global convergence in O(N·|T|), projection soundness, termination, multi-module convergence, and order-independence on

What carries the argument

The Genericable template C(x) = <extendToBe, declaredToBe, hasToBe, definedToBe> is the load-bearing object. extendToBe ascends from NOTHING by join; hasToBe and definedToBe descend from ANY by meet; declaredToBe is a single-assignment declaration fence. requiredShape(x) is the meet of hasToBe and definedToBe. Call-time projection creates a fresh session, sets the call-local coverage to norm(extendToBe ⊔ t_v), and checks the validity chain extendToBe ⪯ t'_x ⪯ declaredToBe ⪯ requiredShape. Supporting machinery includes an eight-rule structural matching preorder (reflexivity, transitivity, top/bottom, primitive promotion, width subtyping, function variance, array covariance, open sum rules) wi

Load-bearing premise

The benchmark comparison stands or falls on the premise that the manually adapted carrier ports preserve the difficulty and oracle semantics of the original Python facts, so that the engine's answers on the ports and the published baseline's answers on the originals measure the same inference task.

What would settle it

Re-run the 28 discordant facts (and ideally all 513) on unmodified Python sources in the original benchmark harness using the engine's Python front end; if the native exact-match count falls below the baseline's 485, or if any port turns out to encode the expected type in its structure, the headline empirical claim is not supported.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Zero-annotation recovery of exact types becomes feasible in a supported fragment, so AOT compilers and IDE checks can run on unannotated dynamic-language code without a learned model.
  • Multicall reuse is safe: because ordinary calls project a fresh session and never rewrite the definition template, independent calls cannot pollute each other's inferred types.
  • Fluent chains over inherited types keep the concrete receiver type after every step, so LLM-driven navigation can compute legal next operators before the model emits text, without F-bounded polymorphism or self-type annotations.
  • The O(N·|T|) convergence and order-independence results make the engine embeddable in multi-module builds with deterministic, order-stable output.
  • On paired ports of a 513-fact benchmark, the deterministic engine's exact score (513/513) exceeds the strongest published LLM prompting baseline (485/513), with every discordant pair favoring the engine.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Going beyond the paper: the decisive test is native evaluation — running the same inference on unmodified Python sources in the original harness rather than through manually adapted carrier ports; the 513/513 figure does not yet establish that.
  • Going beyond the paper: the four-slot decomposition suggests a general design principle for extensible record calculi — keep value, declaration, context, and structure as provenance-labelled constraints — and could be tested in mainstream structural type checkers.
  • Going beyond the paper: the future-this rule hints that open-world structural typing need not rely on self-type machinery; a testable extension is to desugar fluent chains into explicit record refinements in languages without a this{...} construct.
  • Going beyond the paper: because the benchmark adaptation was authored by the same team that developed the engine, a blind or third-party re-adaptation of the 513 facts would distinguish inference strength from oracle familiarity.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 4 minor

Summary. The paper introduces Generic Constraints Projection (GCP), a zero-annotation type-inference framework for dynamic languages. GCP stores four kinds of type evidence — value coverage, declarations, contextual requirements, and structural operations — in separate monotone slots on a stable definition-time template, and checks each call in a fresh projection session. The paper defines the OEM structural subtyping preorder, a future-this rule for preserving concrete receiver types across fluent chains, and proves monotonicity, local/global convergence, conditional projection soundness, termination, multi-module convergence, and order-independence on a bounded success-state fragment, plus classical evaluation/preservation results for an immutable core language Outline0. The empirical section reports 513/513 exact match on 513 manually adapted Outline ports of TypeEvalPy facts, versus 485/513 for Codestral Q&A on the same fact IDs (McNemar p = 7.45e-9). The paper is candid that this is a carrier-port evaluation, not a run on unmodified Python sources.

Significance. If the results hold, the paper would make several useful contributions: a clean separation of four evidence sources that avoids spurious unification conflicts, a fresh-session projection discipline that prevents cross-call contamination, a receiver-preserving fluent-chain mechanism that does not require F-bounds or self-type annotations, and a deterministic inference engine whose formal convergence and termination properties are stated explicitly. The paper also deserves credit for being unusually explicit about its scope: the success-state fragment, the read-only premise, the conditionality of Theorem 4.4, and the carrier-port nature of §8 are all flagged. The formal development is internally plausible, though the proofs are conventional paper proofs and the paper itself lists mechanization as future work. The main risk is the empirical claim: the 513/513 headline depends on an unauditable comparison between author-written Outline ports and an LLM baseline's published answers on the original Python templates, and on a closed-world numeric reporting mapping that may erase genuine type distinctions.

major comments (4)
  1. [§8.1, §8.4] The central empirical claim — GCP 513/513 versus Codestral 485/513 on 'the same fact IDs' — is not currently auditable. The comparison is between GCP on author-written Outline ports and Codestral's published answers on the original Python templates; the per-row PORTABLE/ADAPTED manifest is withheld with the artifact; and §8.4 admits the engine was developed with access to the TypeEvalPy corpus. As it stands, the headline could reflect adaptation choices or label-aware development rather than inference strength. This is load-bearing for Contribution C5. Please either (a) release the per-row manifest and adaptation rules, (b) report a py2asf native-Python result on unmodified TypeEvalPy sources, or (c) explicitly demote the 513/513 claim to a feasibility demonstration rather than a paired competitive result.
  2. [§8.1] The closed-world numeric reporting mapping (Number and String|Number reported as int at integer-witness sites) aligns the engine's carrier-level types to the frozen oracle vocabulary. This mapping is uniform and documented, but it can turn a genuinely imprecise inferred type into an exact label match. Since exact-match is the only metric reported, the 513/513 score may overstate inference precision. Please report both the raw principal types and the mapped labels per fact, or at least give a sensitivity analysis showing how many exact matches survive without the mapping. Without this, the phrase 'exact match' is misleading about the engine's actual precision.
  3. [§4.8, Theorem 4.4 and Definition 4.2] Theorem 4.4's main clause is close to a restatement of Definition 4.2: the projection function is defined to return a substitution only when the canonical call-local type satisfies the validity chain. Stating this as a soundness theorem gives the appearance of a non-trivial result when the proof consists mostly of unpacking the definition. The paper should either reframe Theorem 4.4 as a definitional consistency lemma, or state a genuinely non-circular soundness claim — e.g., that successful projection implies the actual argument satisfies requiredShape and the declaration fence, and that the variance-aware substitution of the return type is a safe approximation of the runtime result. The latter is claimed in the proof sketch but is not stated as part of the theorem's conclusion.
  4. [§8.3] The capability ablation suite uses only 24 mechanism observations (15 positive, 9 expected rejects), with no statistical analysis or error margins. This is acknowledged as 'separate' and 'not folded into the §8.2 denominator,' which is good, but the text draws conclusions from counts this small ('the same engine, unmodified, rejects the paired ill-typed programs'). Please soften these claims or provide the specific program list so readers can judge how representative the 24 observations are. This is a secondary issue relative to the benchmark-port problem, but it affects the strength of the capability claims.
minor comments (4)
  1. [§3.2] Rule R8c (Option–Option subtyping) is used in the Appendix A transitivity proof but is omitted from the eight rules listed in the main text. Please state it in §3.2 as well, or explicitly refer forward to the appendix.
  2. [Figure 5 caption] The caption says 'the largest gaps are indirect_calls and returns,' but Table 3 lists categories assignments, direct_calls, functions, lambdas, lists, dicts, returns, classes — there is no indirect_calls category. Please align the caption with the actual category names.
  3. [§5 and elsewhere] The notation 'future this' and 'this{...}' is used with inconsistent spacing and capitalization across the text; please standardize.
  4. [§4.4, Definition 4.1c] The norm function is defined as a 'fixed, deterministic function' but its behavior on records and options is only described informally. For a paper that emphasizes determinism and order-independence, a few more examples or a reference to the artifact would help.

Circularity Check

2 steps flagged

Two formal theorems restate their own definitions (projection soundness echoes Definition 4.2; future-this preservation is built into the ⊕ operator), while the benchmark comparison is an auditability risk rather than a definitional loop.

specific steps
  1. self definitional [§4.4, Definition 4.2; §4.8, Theorem 4.4]
    "project(C_def(x), τ_v) creates a fresh projection session, sets τ'_x = norm(τ_e ⊔ τ_v), and returns the substitution σ=[x→τ'_x] if this least coverage type satisfies the applicable validity chain."

    Theorem 4.4 states: 'if a call-time session successfully derives project(C_def(x), τ_v)=σ, then its canonical call-local type τ'_x = norm(τ_e ⊔ τ_v) satisfies the applicable validity chain.' But Definition 4.2 defines successful projection precisely as that same validity chain holding. The theorem's main clause is therefore a restatement of the definition of success; the additional conclusion that the actual argument satisfies the required shape follows by transitivity from the chain already required by the definition. The substitution-safety part via Lemma A.3 is independent, but the headline 'projection soundness' claim is true by construction.

  2. self definitional [§5.3, T-ThisExtend; §5.4, ⊕ properties; §5.5, Theorem 5.1]
    "For any f_i ∈ fields(τ_recv) that is replaced (under the default merge rule), (τ_recv⊕{f_i : σ_i}).f_i ⪯ τ_recv.f_i. ... Combined with width preservation, this yields the subtype relation (τ_recv⊕...)⪯τ_recv for the default case."

    T-ThisExtend defines the return type of this{f_1=v_1,...,f_n=v_n} as τ_recv ⊕ {f_i:σ_i}. In §5.4, ⊕ is defined to satisfy narrowing covariance and width preservation, explicitly giving (τ_recv⊕...)⪯τ_recv and the preservation of untouched fields. Theorem 5.1 then asserts exactly these two defining properties of ⊕ after a method call. The only extra ingredient is the dispatch-time binding of this to the receiver, which the typing rule already stipulates. Thus the 'receiver retention' theorem is baked into the operator and rule definitions rather than derived from more basic semantics.

full rationale

Most of the derivation is self-contained. Theorems 4.2–4.3, 4.5–4.7 are proved from finite-height and monotonicity arguments over the abstract domain; Theorems P, T, T-this, and C are standard subject-reduction results for Outline0 with independent inductions. No load-bearing self-citation appears: companion papers [6, 48] are pointers to applications, not premises of the formal results. The benchmark is candidly disclosed as a carrier-port evaluation (§8.1, §8.4) with the per-row manifest withheld and the engine developed with access to TypeEvalPy; that is an auditability and port-fairness threat to the empirical claim, not a circular derivation, since no quoted step fits parameters to oracle labels and then repackages the fit as a prediction. However, two formal 'guarantees' reduce to their own definitions. Definition 4.2 makes projection success identical to satisfying the validity chain, so Theorem 4.4's main clause restates the definition; and Theorem 5.1's preservation clauses are the defining properties of the ⊕ operator in §5.4, with the receiver-binding stipulated by T-ThisExtend. These are design-by-construction statements rather than independently derived consequences, giving partial circularity in the formal layer while leaving the convergence and order-independence results, and the non-circular benchmark caveats, intact.

Axiom & Free-Parameter Ledger

6 free parameters · 7 axioms · 3 invented entities

The formal claims are conditional on a stack of explicitly stated assumptions: read-only variance, success-state subspace, per-program bounded |T| set by tunable engineering bounds, carrier-scope semantics, and the immutable Outline0 core for the L2 results. The empirical claim adds non-auditable conventions: manual port fidelity and closed-world vocabulary reporting. The invented entities (Genericable, This decorator, this{...}, the Outline language) are formalism-internal with no external falsifiable handle; nothing physical is postulated.

free parameters (6)
  • structural path depth bound = tunable per program
    §2.2: finite upper bound on field-path depth to keep T of bounded height; |T| in all convergence bounds depends on it.
  • Option/Union width bound = tunable per program
    §2.2: bounds Option/Union arity; affects |T| and the R8 rule applicability.
  • generic-instantiation depth bound = tunable per program
    §2.2: needed for projection termination (Theorem 4.5).
  • monomorphic-specialisation count bound = tunable per program
    §2.2: bounds the number of specialisations of a single generic.
  • maxRounds safety net = engineering parameter
    Algorithm 1 (§4.7): Theorem 4.7 order-independence requires maxRounds not to truncate; the paper admits it occasionally triggers in production.
  • closed-world numeric reporting mapping = Number reported as int at integer-witness sites
    §8.1 mapping 1: aligns the engine's principal types to the TypeEvalPy oracle vocabulary; a reporting convention tuned so that 'exact match' is measured against the benchmark's label set.
axioms (7)
  • domain assumption Read-only premise: record fields and array elements treated as read-only for OEM variance (R5, R7)
    §3 preamble; without it width subtyping and array covariance become invariant; Theorem 4.4 and Lemma 4.1 depend on it.
  • domain assumption Success-state subspace: all theorems exclude ERROR states (uninhabited meets, failed chains, DECL_CONFLICT)
    Definition 4.3; Theorems 4.1–4.7, P, T, T-this, C are all conditional on it.
  • domain assumption Bounded height |T| via per-program engineering bounds (widening to ANY / recursive summaries)
    §2.2; required for Theorems 4.2–4.6 and projection termination.
  • domain assumption Carrier-scope: Outline parameter-slot semantics; Python parameter-name rebinding modeled as a fresh local binding
    §4.6 R2; Theorem 4.4 is conditional on this carrier restriction.
  • domain assumption Immutable core Outline0 (no mutation, modules, async, Poly dispatch) for the big-step results
    Appendix B.2; Theorems P, T, T-this, C are L2 results for Outline0 only.
  • standard math OEM R1–R8 as the subtyping relation, a refinement of the standard structural-subtyping calculus
    §3.2; Theorem 3.1 preorder proof depends on the rules as stated, including R8c (derivable from R8a/R8b without transitivity) and the read-only variance adaptations.
  • domain assumption Environment-respect conditions ρ |= Γ, closure outlines carrying stable L1 types, runtime ⊕_r agreeing with type-level ⊕
    Appendix B.2–B.4; needed for Theorems T, T-this, C.
invented entities (3)
  • Genericable G[C] — type variable carrying a four-dimensional constraint tuple no independent evidence
    purpose: Unresolved parameter/local placeholder holding extendToBe/declaredToBe/hasToBe/definedToBe slots
    Framework-internal construct (§2.2, §4.2); necessity is witnessed only by the author-written regression suite (§4.1.1); no falsifiable handle outside the framework.
  • This(τ_recv, τ_def) decorator and this{...} copy-with-extension construct (with ⊕ operator) no independent evidence
    purpose: Receiver/definer distinction enabling future-this receiver preservation across fluent chains
    §5.2–5.4; Theorem 5.1 reduces to the defining properties of ⊕; construct exists only in the invented Outline carrier and is inapplicable to the Python carrier (§7.2).
  • Outline language itself no independent evidence
    purpose: Carrier language hosting the GCP formalization and the TypeEvalPy ports
    §2.1; invented for this paper; the empirical evaluation runs on the authors' own Outline ports of TypeEvalPy, not on a pre-existing language or corpus.

pith-pipeline@v1.3.0-alltime-deepseek · 54115 in / 26261 out tokens · 257042 ms · 2026-08-01T12:00:16.420662+00:00 · methodology

0 comments
read the original abstract

Type inference for dynamically typed languages must reconcile four qualitatively different sources of evidence: assigned values, explicit declarations, contextual requirements, and structural operations. Existing approaches often combine them into one constraint set, causing spurious conflicts or requiring annotations. We present Generic Constraints Projection (GCP), a zero-annotation inference framework that stores these sources in four monotone slots on a stable definition-time template and evaluates each call in a fresh projection session, preventing cross-call contamination while specializing return types. GCP uses Outline Equational Matching, an open structural preorder, and a future-this projection rule that preserves concrete receiver types across fluent chains and subtype extensions. On the success-state fragment of a bounded type domain, we prove monotonicity, local and global fixed-point convergence, conditional projection soundness, termination, multi-module convergence, and order independence. For an immutable core language, we also prove big-step evaluation existence, type preservation, runtime receiver retention, and projection-evaluation coherence. We instantiate GCP in Outline for typed ontology worlds and in a Python annotation-recovery pipeline. On 513 manually adapted, fact-paired Outline ports of TypeEvalPy cases, GCP obtains 513/513 exact matches, compared with 485/513 for the published Codestral Q&A baseline on the same fact IDs (two-sided exact McNemar p = 7.45e-9). This is a carrier-port evaluation in TypeEvalPy's closed-world Python vocabulary, not a run on unmodified Python sources.

Figures

Figures reproduced from arXiv: 2607.19693 by Qunhui Zhang.

Figure 1
Figure 1. Figure 1: Mixed-direction constraint geometry for a definition [PITH_FULL_IMAGE:figures/full_fig_p018_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Two-phase GCP semantics. Definition-time evidence converges to a stable Genericable template. An ordinary call projects a [PITH_FULL_IMAGE:figures/full_fig_p019_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Higher-order projection flow for lift. Forward flow supplies the concrete argument to a copied entity template; backward flow carries the body requirement through pred and sel inside the same projection session. The stable definition template remains unchanged. reusable definition template; only the projection session contains alice’s concrete specialization and backward-flow refinements. The same session-… view at source ↗
Figure 4
Figure 4. Figure 4: Receiver preservation on the running example [PITH_FULL_IMAGE:figures/full_fig_p027_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Per-category exact-match rates for GCP versus Codestral Q&A on all 513 TypeEvalPy micro-benchmark fact IDs. GCP is 100% [PITH_FULL_IMAGE:figures/full_fig_p035_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. VirtualSet: Typed Ontology Worlds as an LLM Generation Target for Grounded Queries and Guarded Decisions

    cs.PL 2026-07 conditional novelty 6.0

    A typed ontology-expression target for LLMs beat glossary-matched direct SQL on BIRD (67.5% vs 63.5%) and intercepted all 20 hallucinated action bodies in a 30-body corpus.

Reference graph

Works this paper leans on

48 extracted references · 6 canonical work pages · cited by 1 Pith paper · 1 internal anchor

  1. [1]

    Alexander Aiken and Edward L. Wimmers. 1993. Type Inclusion Constraints and Type Inference. InProceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA ’93). ACM, New York, NY, USA, 31–41. doi:10.1145/165180.165188

    arXiv 1993

  2. [2]

    Apple. 2026. The Swift Programming Language. https://docs.swift.org/swift-book/documentation/the-swift-programming-language/. Accessed 2026-07-16

    2026

  3. [3]

    Anonymous Authors. 2025. Generic Constraints Projection for Zero-Annotation Python AOT Compilation. (2025). Manuscript under review

    2025

  4. [4]

    Anonymous Authors. 2026. GCP type engine artifact. Artifact URL withheld for double-blind review. Will be released upon acceptance

    2026

  5. [5]

    Anonymous Authors. 2026. Outline language artifact. Artifact URL withheld for double-blind review. Will be released upon acceptance

    2026

  6. [6]

    Anonymous Authors. 2026. Zero-Annotation Python Type Recovery with Generic Constraints Projection. (2026). Companion systems paper; arXiv preprint forthcoming

    2026

  7. [7]

    Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. 2023. Prompting Is Programming: A Query Language for Large Language Models.Proceedings of the ACM on Programming Languages7, PLDI, Article 186 (2023), 24 pages. doi:10.1145/3591300

    doi:10.1145/3591300 2023

  8. [8]

    Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding TypeScript. InECOOP 2014 – Object-Oriented Programming (Lecture Notes in Computer Science, Vol. 8586). Springer, Berlin, Heidelberg, 257–281. doi:10.1007/978-3-662-44202-9_11

    work page doi:10.1007/978-3-662-44202-9_11 2014

  9. [9]

    Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T

    Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin C. Pierce. 1995. On Binary Methods. Theory and Practice of Object Systems1, 3 (1995), 221–242. doi:10.1002/j.1096-9942.1995.tb00019.x

    arXiv 1995

  10. [10]

    Mitchell

    Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C. Mitchell. 1989. F-Bounded Polymorphism for Object-Oriented Programming. InProc. of FPCA. ACM, New York, NY, USA, 273–280. doi:10.1145/99370.99392

    arXiv 1989

  11. [11]

    Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism.Comput. Surveys17, 4 (Dec. 1985), 471–523. doi:10.1145/6041.6042

    arXiv 1985

  12. [12]

    Danny Dubé and Marc Feeley. 2002. A Demand-Driven Adaptive Type Analysis. InProceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming. ACM, New York, NY, USA, 84–97. doi:10.1145/581478.581487 Generic Constraints Projection: Four-Dimensional Type Inference for Dynamic Languages 61

    arXiv 2002

  13. [13]

    Smith, and Valery Trifonov

    Jonathan Eifrig, Scott F. Smith, and Valery Trifonov. 1995. Sound Polymorphic Type Inference for Objects. InProceedings of the 10th Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM, New York, NY, USA, 169–184. doi:10.1145/217838. 217858

    work page doi:10.1145/217838 1995

  14. [14]

    Google. 2017. pytype: A static type analyzer for Python code. Software. https://github.com/google/pytype

    2017

  15. [15]

    Ivan Levkivskyi, Jukka Lehtosalo, and Łukasz Langa. 2017. PEP 544 – Protocols: Structural subtyping (static duck typing). Python Enhancement Proposal 544. https://peps.python.org/pep-0544/

    2017

  16. [16]

    Liskov and Jeannette M

    Barbara H. Liskov and Jeannette M. Wing. 1994. A Behavioral Notion of Subtyping.ACM Transactions on Programming Languages and Systems16, 6 (Nov. 1994), 1811–1841. doi:10.1145/197320.197383

    arXiv 1994

  17. [17]

    Kuang-Chen Lu, Ben Greenman, Carl Meyer, Dino Viehland, Aniket Panse, and Shriram Krishnamurthi. 2023. Gradual Soundness: Lessons from Static Python.The Art, Science, and Engineering of Programming7, 1 (2023), 2:1–2:40. doi:10.22152/programming-journal.org/2023/7/2

    work page doi:10.22152/programming-journal.org/2023/7/2 2023

  18. [18]

    Haoran Luo, Haihong E, Zichen Tang, Shiyao Peng, Yikai Guo, Wentai Zhang, Chenghao Ma, Guanting Dong, Meina Song, Wei Lin, Yifan Zhu, and Anh Tuan Luu. 2024. ChatKBQA: A Generate-then-Retrieve Framework for Knowledge Base Question Answering with Fine-tuned Large Language Models. InFindings of ACL. Association for Computational Linguistics, Bangkok, Thaila...

    2024

  19. [19]

    Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Sean Welleck, Bodhisattwa Prasad Majumder, Shashank Gupta, Amir Yazdanbakhsh, and Peter Clark. 2023. Self-Refine: Iterative Refinement with Self-Feedback. InAdvances in Neural Information Processing Systems, Vol. 36...

    doi:10.52202/075280-2019 2023

  20. [20]

    Meta. 2014. Flow, a New Static Type Checker for JavaScript. https://engineering.fb.com/2014/11/18/web/flow-a-new-static-type-checker-for- javascript/. Accessed 2026-07-16

    2014

  21. [21]

    Microsoft. 2019. Pyright: Static Type Checker for Python. Software. https://github.com/microsoft/pyright

    2019

  22. [22]

    Microsoft. 2023. TypeChat: Types as the Interface Between Natural Language and Application Schema. https://github.com/microsoft/TypeChat

    2023

  23. [23]

    Microsoft. 2026. TypeScript. https://www.typescriptlang.org/. Accessed 2026-07-16

    2026

  24. [24]

    Microsoft. 2026. The TypeScript Handbook. https://www.typescriptlang.org/docs/handbook/intro.html. Accessed 2026-07-16

    2026

  25. [25]

    Microsoft. 2026. TypeScript Handbook: Polymorphic this Types. https://www.typescriptlang.org/docs/handbook/advanced-types.html# polymorphic-this-types. Accessed 2026-07-16

    2026

  26. [26]

    Robin Milner. 1978. A Theory of Type Polymorphism in Programming.J. Comput. System Sci.17, 3 (Dec. 1978), 348–375. doi:10.1016/0022- 0000(78)90014-4

    doi:10.1016/0022- 1978

  27. [27]

    Mir, Evaldas Latoškinas, Sebastian Proksch, and Georgios Gousios

    Amir M. Mir, Evaldas Latoškinas, Sebastian Proksch, and Georgios Gousios. 2022. Type4Py: Practical Deep Similarity Learning-Based Type Inference for Python. InProceedings of the 44th International Conference on Software Engineering. ACM, New York, NY, USA, 2241–2252. doi:10.1145/3510003. 3510124

    doi:10.1145/3510003 2022

  28. [28]

    Mistral AI. 2024. Codestral. https://mistral.ai/news/codestral. Codestral-v0.1-22b; TypeEvalPy Q&A baseline in thesoapsartifact

    2024

  29. [29]

    Alan Mycroft. 1984. Polymorphic Type Schemes and Recursive Definitions. InProceedings of the International Symposium on Programming (Lecture Notes in Computer Science, Vol. 167). Springer, Berlin, Heidelberg, 217–228. doi:10.1007/3-540-12925-1_41

    work page doi:10.1007/3-540-12925-1_41 1984

  30. [30]

    mypy contributors. 2026. mypy Documentation. https://mypy.readthedocs.io/en/stable/. Accessed 2026-07-16

    2026

  31. [31]

    Yun Peng, Cuiyun Gao, Zongjie Li, Bowei Gao, David Lo, Qirun Zhang, and Michael R. Lyu. 2022. Static Inference Meets Deep Learning: A Hybrid Type Inference Approach for Python. InProceedings of the 44th International Conference on Software Engineering. ACM, New York, NY, USA, 2019–2030. doi:10.1145/3510003.3510038

    arXiv 2022

  32. [32]

    Benjamin C. Pierce. 2002.Types and Programming Languages. MIT Press, Cambridge, MA, USA

    2002

  33. [33]

    Pierce and David N

    Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference.ACM Transactions on Programming Languages and Systems22, 1 (Jan. 2000), 1–44. doi:10.1145/345099.345100

    arXiv 2000

  34. [34]

    Gabriel Poesia, Oleksandr Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. 2022. Synchromesh: Reliable Code Generation from Pre-trained Language Models. International Conference on Learning Representations. https://openreview.net/forum?id= KmtVD97J43e

    2022

  35. [35]

    1998.Type Inference in the Presence of Subtyping: From Theory to Practice

    François Pottier. 1998.Type Inference in the Presence of Subtyping: From Theory to Practice. Technical Report RR-3483. INRIA. https://inria.hal. science/inria-00073205

    1998

  36. [36]

    François Pottier and Didier Rémy. 2005. The Essence of ML Type Inference. InAdvanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Cambridge, MA, USA, 389–489

    2005

  37. [37]

    Mohammadreza Pourreza and Davood Rafiei. 2023. DIN-SQL: Decomposed In-Context Learning of Text-to-SQL with Self-Correction. InAdvances in Neural Information Processing Systems, Vol. 36. Curran Associates, Inc., Red Hook, NY, USA, 36339–36348. doi:10.52202/075280-1577

    work page doi:10.52202/075280-1577 2023

  38. [38]

    J. A. Robinson. 1965. A Machine-Oriented Logic Based on the Resolution Principle.J. ACM12, 1 (1965), 23–41. doi:10.1145/321250.321253

    arXiv 1965

  39. [39]

    Rust Project Developers. 2026. The Rust Reference: Paths andSelf. https://doc.rust-lang.org/reference/paths.html. Accessed 2026-07-16

    2026

  40. [40]

    Chieri Saito and Atsushi Igarashi. 2009. Matching ThisType to Subtyping. InProceedings of the 24th Annual ACM Symposium on Applied Computing. ACM, New York, NY, USA, 1851–1858. doi:10.1145/1529282.1529699

    arXiv 2009

  41. [41]

    Scala Center. 2026. Scala Documentation: Self-Type. https://docs.scala-lang.org/tour/self-types.html. Accessed 2026-07-16

    2026

  42. [42]

    Torsten Scholak, Nathan Schucher, and Dzmitry Bahdanau. 2021. PICARD: Parsing Incrementally for Constrained Auto-Regressive Decoding from Language Models. InProceedings of the 2021 Conference on Empirical Methods in Natural Language Processing. Association for Computational 62 Zhang Linguistics, Online and Punta Cana, Dominican Republic, 9895–9901. doi:10...

    doi:10.18653/v1/2021.emnlp-main.779 2021

  43. [43]

    Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. 2023. Reflexion: Language Agents with Verbal Reinforcement Learning. InAdvances in Neural Information Processing Systems, Vol. 36. Curran Associates, Inc., Red Hook, NY, USA, 8634–8652. doi:10.52202/075280- 0377

    doi:10.52202/075280- 2023

  44. [44]

    Mir, Li Li, and Eric Bodden

    Ashwin Prasad Shivarpatna Venkatesh, Samkutty Sabu, Jiawei Wang, Amir M. Mir, Li Li, and Eric Bodden. 2024. TypeEvalPy: A Micro-benchmarking Framework for Python Type Inference Tools. InProceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings. ACM, New York, NY, USA, 49–53. doi:10.1145/3639478.3640033

    arXiv 2024

  45. [45]

    Siek and Walid Taha

    Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. InProceedings of the Scheme and Functional Programming Workshop. University of Chicago, Chicago, IL, USA, 81–92

    2006

  46. [46]

    Bing Wang, Changyu Ren, Jian Yang, Xinnian Liang, Jiaqi Bai, Linzheng Chai, Zhao Yan, Qian-Wen Zhang, Di Yin, Xing Sun, and Zhoujun Li. 2025. MAC-SQL: A Multi-Agent Collaborative Framework for Text-to-SQL. InProceedings of the 31st International Conference on Computational Linguistics. Association for Computational Linguistics, Abu Dhabi, UAE, 540–557. ht...

    2025

  47. [47]

    Willard and Rémi Louf

    Brandon T. Willard and Rémi Louf. 2023. Efficient Guided Generation for Large Language Models. arXiv preprint arXiv:2307.09702. doi:10.48550/ arXiv.2307.09702

    Pith/arXiv arXiv doi:10.48550/arxiv.2307.09702 2023

  48. [48]

    Qunhui Zhang. 2026. VirtualSet: Typed Ontology Worlds as an LLM Generation Target for Grounded Queries and Guarded Decisions. arXiv:2607.18821 [cs.PL] doi:10.48550/arXiv.2607.18821

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2607.18821 2026