{"id":"f906247f-d4c1-4872-b3f4-7f845033be84","arxiv_id":"1908.06478","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":1,"one_line_summary":"A GHC plugin adapts the JVFH type-based amortized analysis to GHC Core, automatically deriving linear resource bounds for a subset of Haskell programs.","lead":"This paper presents a compiler plugin that automatically derives linear upper bounds on the time or memory use of Haskell programs by inspecting GHC Core, the compiler's internal language. It is a step toward practical resource analysis for lazy languages, though the prototype lacks polymorphism support and a soundness proof.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central claim depends on soundness of adapted typing rules; paper admits no proof and documents a concrete unsound reused rule, so upper-bound status is not established.","rationale":"The reader's weakest assumption—unproven soundness of the adapted typing rules—is exactly the load-bearing concern I find. The paper is honest about this in Section 8, and the LETREC counterexample in Sections 5 and 7 turns a theoretical risk into a concrete one: a rule inherited from JVFH was shown to under-approximate, which means the adaptation process itself can introduce or inherit unsoundness. Since the central claim is specifically that the analysis derives upper bounds, any under-approximation undermines the claim, not just a minor flaw. I give credit for the working prototype, the reproducible comparisons against the JVFH demo, and the clear reporting of the bug and its fix; these are real evidence that the tool works on the tested examples. But they do not establish the general upper-bound claim. A differential test against an executable cost semantics would provide strong evidence, and a formal soundness proof for the supported Core fragment would settle the matter. Because the paper itself scopes the result as an initial implementation and the reader's CONDITIONAL verdict already reflects this, I do not see a reason to change the verdict; the appropriate bar is that the soundness question must be addressed or explicitly scoped as future work.","tokens_in":12028,"tokens_out":3490,"duration_ms":37492,"concrete_test":"Implement a small cost semantics for the Core fragment of Figure 2 and instrument the tool to output the full derivation tree with all numeric annotations for each program. Then, for a corpus covering each adapted rule (including the Fibonacci letrec with ⊳ disabled, map over an infinite list, and case expressions with default alternatives), compute both the tool's bound and the exact cost under the semantics (with memoized thunk evaluation), and check bound ≥ cost for every program. If any program violates the inequality, the upper-bound claim is refuted; if all pass, the concern is reduced but a proof is still required for full soundness.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that the tool derives linear upper bounds on resource usage for a substantial subset of Haskell. This requires every typing rule in the adapted system to be sound with respect to an operational cost semantics for the supported fragment of GHC Core. Section 8 explicitly states no such soundness proof exists. More importantly, Sections 5 and 7 document a counterexample to soundness in a rule that was reused almost unchanged: the LETREC GC rule, using the ⊳ operator, derives constant cost for an infinite Fibonacci list that actually has linear cost. The authors disable the operator, but the incident shows that 'reused from JVFH' cannot be treated as a soundness guarantee for the other adapted rules—APP GC, CONS GC, LET GC, CASE ALG GC, CASE LIT GC, TYABS GC, TYAPP GC, TYLET GC—several of which are new or substantially modified. The workarounds in Section 4 (primitive types as empty algebraic types, type abstractions as artificial functions) also change the intended semantics of the type syntax, so the unmodified JVFH relations (Sharing, ⊳) are not automatically justified in this embedding. Consequently, the reported annotations are not established upper bounds; they are candidate bounds that happened to pass the tested examples.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a GHC plugin that translates Haskell into GHC Core and applies an adapted JVFH-style amortized-resource-analysis type system to derive linear resource-usage annotations. It describes the Core syntax subset (Figure 2), presents adapted and newly introduced typing rules (Figures 4--7), implements an LP-based constraint solver, and evaluates the tool on examples such as repeat, map, and a Fibonacci list. The paper explicitly states that no soundness proof for the adapted system is provided and reports a concrete under-approximation in the reused LETREC rule, which is disabled as a workaround.","tokens_in":12275,"tokens_out":6709,"duration_ms":69227,"significance":"If the derived annotations were guaranteed upper bounds, the tool would be a useful bridge between JVFH-style amortized analysis and a real-world lazy functional language, and the GHC plugin architecture is a sensible engineering choice. The paper is also honest about its limitations and contributes a concrete counterexample to a previously trusted typing rule, which is a valuable warning for the community. However, the central upper-bound claim is not established, and the reported unsoundness in a reused rule shows that inherited rules cannot be trusted without individual justification; the significance of the contribution is therefore conditional on a soundness argument or a substantially weakened claim.","major_comments":[{"comment":"The central claim that the type system derives linear upper bounds is not established. Section 8 states that the adapted type system has not been formally proven sound and that an operational cost semantics for GHC Core would be needed for such a proof. Without that proof, the annotations produced by the tool are candidate bounds rather than guaranteed upper bounds; the abstract and conclusion should be revised accordingly, or the proof should be supplied.","section":"Abstract; Section 8"},{"comment":"The Fibonacci counterexample described in Sections 5 and 7 demonstrates that the reused LETREC GC rule, with the operator, under-approximates resource usage: it yields a constant-cost type for an infinite list whose evaluation cost is linear. The authors report that they reproduced the same failure in the original JVFH analysis, so reusing a rule from JVFH does not make it sound in this setting. Each adapted and newly introduced rule (APP GC, CONS GC, LET GC, CASE ALG GC, CASE LIT GC, TYABS GC, TYAPP GC, and TYLET GC) needs an individual soundness argument with respect to the chosen cost model; disabling the operator is not a proof for the remaining rules.","section":"Section 5, LETREC GC rule"},{"comment":"The workarounds for primitive types and type abstractions alter the intended semantics of the JVFH type syntax. Representing primitive types as the empty algebraic type mu X .{} conflates all primitive values and discards their cost behavior, while replacing forall a. T with mu X .{} -0-> T makes type abstraction look like a function of non-thunk type, violating the invariant that all function arguments are wrapped in thunk types. Because Sharing, subtype, and the operator are defined over the original type structure, reusing them without modification requires a formal justification or a proof that the embedding is semantics-preserving; the current discussion does not provide this.","section":"Section 4, Type syntax workarounds"}],"minor_comments":[{"comment":"The annotation uses |T| and |B| and the abbreviation mu T1.{} without defining the notation; please define the number of fields and the empty algebraic type in one place.","section":"Figure 5, CONS GC rule"},{"comment":"The claim that the undecidability of System F type inference also applies to STG because STG lacks type information is speculative and not needed for the argument; either support it with a reference to a precise statement or remove it.","section":"Section 3"},{"comment":"The statement that type variables may only be used as recursive references conflicts with the later discussion of free type variables in the polymorphism workaround; please clarify the status of free type variables in the type syntax.","section":"Section 4"},{"comment":"A link to the implementation or a repository would improve reproducibility; the paper currently refers to a thesis and an online demo but does not give an artifact location for the tool itself.","section":"Section 6"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is unusually transparent about its own limitations, which I credit. The main question for the editor is whether this venue accepts work-in-progress tool papers: if the bar is a verified analysis, the paper would need either a soundness proof or a recasting as a tool demonstration with the upper-bound claim removed from the abstract. I believe a major revision that honestly reframes the contribution and adds at least a soundness sketch for the remaining rules is achievable and would make the paper valuable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is an honest, useful proof-of-concept. It adapts JVFH amortized analysis to GHC Core and ships a working GHC plugin. The most valuable piece is the negative result: the Fibonacci example reveals that the reused LETREC rule, with the ⊳ operator, can under-approximate cost. The authors disable the operator rather than return wrong bounds; that is a genuine finding about prior work and a good engineering decision, documented clearly.\n\nWhat's new: applying JVFH to actual Haskell via GHC Core, with adapted and new rules for Core's case expressions, applications with non-variable arguments, type abstraction and application, and literals. The structural rules and the Sharing relation are reused wholesale, which is reasonable given the type syntax is unchanged. The implementation is real — the plugin architecture, the LP solving, the hard-coded primitives, and several end-to-end examples are all there.\n\nWhere it's soft: the central claim is not established. Section 8 explicitly says there is no soundness proof for the adapted system, and the Fibonacci incident shows that reuse is not a soundness guarantee. The workarounds — primitive types as empty algebraic types, type abstractions as artificial functions — change the intended semantics of the type syntax, so the borrowed relations (Sharing, ⊳) may not mean what they did in JVFH. The comparisons to JVFH are sanity checks, not a formal equivalence. So the reported annotations are candidate bounds, not proven upper bounds; the abstract overstates this. For a workshop paper this is acceptable if the claims are scoped accordingly, but for a journal the soundness gap would need real work.\n\nThe lack of polymorphism, newtype support, and multi-module analysis is honestly discussed. The paper reads like a master's thesis summary, with the scope of a first implementation — clear, but not a mature system.\n\nWho it's for: researchers working on type-based resource analysis, especially for lazy languages, and anyone building GHC plugins. The Fibonacci counterexample is worth knowing even if you never use the tool.\n\nMy recommendation: send it to peer review. It is close to acceptable for a workshop if the authors revise the abstract and conclusion to say 'candidate upper bounds' and clearly state the unsoundness implications. The negative result alone makes it worth publishing.","headline":"An honest proof-of-concept tool paper that adapts JVFH amortized analysis to GHC Core and uncovers a real unsoundness in a previous rule, but the upper-bound claim is not formally established.","tokens_in":12816,"tokens_out":2495,"would_cite":false,"duration_ms":24436,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that a GHC plugin can adapt the JVFH type-based amortized analysis to GHC Core and automatically derive linear upper bounds on resource use for actual Haskell programs.","keywords":["amortized analysis","resource bounds","Haskell","GHC Core","type-based cost analysis","lazy evaluation","linear programming","compiler plugin"],"falsifier":"Instrument a compiled GHC Core program with an allocation counter, run the paper’s analysis on a set of mutually recursive infinite-list programs, and look for any case where the returned upper bound is below the measured allocation; the Fibonacci example shows exactly this failure mode, and the paper’s fix would be vindicated by finding no further such cases.","tokens_in":11798,"feed_emoji":"⚙️","tokens_out":9713,"duration_ms":92926,"temperature":0.7,"pith_summary":"Static resource analysis for lazy languages has mostly worked on small custom languages, because laziness makes every subexpression a potential thunk and costs depend on evaluation order. This paper argues that the gap can be closed by running an adapted version of the JVFH type-based amortized analysis—originally designed for a custom lazy language—on GHC Core, the intermediate representation GHC already generates for real Haskell programs. A GHC plugin lifts Haskell into Core automatically, the type system derives annotated types whose numeric annotations are linear upper bounds on resources (memory allocations or runtime steps), and an LP solver fixes the numbers. The payoff is that ordinary Haskell with list comprehensions, partial applications, and infinite lists can be analyzed without hand translation, and the analysis can expose differences such as constant-space versus linear-space versions of repeat. The paper is explicit that the adaptation is not yet formally proven sound, and it reports a counterexample that forced a soundness fix in one reused rule.","feed_headline":"GHC plugin derives linear resource bounds on real Haskell","feed_subtitle":"Adapting a lazy-language type system to GHC Core automates cost analysis and exposes an unsound rule.","key_machinery":"The load-bearing object is the adapted JVFH type system on GHC Core. JVFH—a custom lazy functional language designed for analyzability—annotates every resource-relevant construct with numeric potential: a function type $A \\xrightarrow{q} B$ costs at most $q$ to apply, a thunk type $T_q(A)$ costs at most $q$ to force, and a recursive algebraic type $\\mu X.\\{c:(q,A)\\}$ attaches $q$ resources to each constructor, redeemable on pattern match. The core typing judgment is $\\Gamma \\vdash_p^q e : T$, read as “evaluating $e$ to weak head normal form—the outermost constructor or $\\lambda$—uses at most $p$ resources and leaves at least $q$ available.” Sharing judgments split a variable’s potential among several uses so potential is not redeemed twice. The derivation produces linear constraints over the annotation variables, and an LP solver picks values that make the typing valid. The adaptation work is concentrated in the syntax-driven rules for Core’s let, case, constructor, literal, and type expressions; the structural rules and type relations are reused verbatim from the JVFH system.","core_discovery":"The central discovery is that most of the JVFH machinery survives the move to GHC Core: the annotated type syntax (function types $A \\xrightarrow{q} B$, thunk types $T_q(A)$, recursive algebraic types $\\mu X.\\{c:(q,A)\\}$), the typing and sharing judgments, and the structural rules transfer unchanged, because they are syntax-independent. Only the syntax-driven rules need reworking, and the paper presents adapted versions for variables, abstraction, application, constructors, let, letrec, pattern matching on algebraic and literal types, and type abstraction and application. These rules turn each expression into a set of linear constraints, which an LP solver resolves into concrete upper bounds. The same adaptation exposed a genuine flaw in the inherited LETREC rule: using the $\\rhd$ operator let the analysis derive constant cost for the infinite Fibonacci list, an under-approximation; the paper disables $\\rhd$, preferring an unsolvable linear program to a wrong bound. The aim is a working prototype that analyzes actual Haskell code, with the JVFH analysis on hand-translated programs serving as the behavioral oracle.","pith_inferences":["The LETREC counterexample implies that every JVFH rule ported to Core should be re-tested on Core’s actual evaluation order; the paper’s failure-safe fix is a template, not a certificate.","A cheap validation experiment is to instrument compiled Core with allocation counters and compare measured allocations against derived bounds on a benchmark set of lazy programs; any under-bound is a candidate unsound rule.","Since the type annotations are linear potentials, the analysis cannot express bounds such as logarithmic or $n \\log n$ without extending the potential language; that limitation is a property of the JVFH-style system, not of GHC Core.","The monomorphization workaround for polymorphism suggests a route toward full polymorphism: replace type abstraction with resource-neutral identity wrappers and only then instantiate, but the paper leaves the necessary type syntax changes open."],"forward_implications":["Programmers analyzing real Haskell modules can obtain concrete annotated types, such as the paper’s result for `map (+1) $ repeat 1 :: [Int]`, which says evaluating the list to its head costs 9 allocations and each additional list node costs at most 3.","Because the input is GHC Core, the analysis runs after compiler optimizations; the paper’s `map1`/`map2` example shows that GHC’s own duplication removal can change a previously analyzable program into one that fails, so bounds are tied to the optimizer’s choices.","The disabled $\\rhd$ operator in LETREC GC makes the tool fail-safe on the Fibonacci-style infinite list, preferring an unsolvable linear program over a constant bound that the code cannot actually achieve.","The stated next steps—polymorphism, newtype coercions, and multi-module support—are concrete barriers; each has a known location in the Core syntax, so progress is incremental rather than requiring a new analysis design."],"supporting_citations":[{"why":"Introduces the amortized analysis method with type-annotated potentials and LP-generated bounds that this line of work builds on.","marker":"[8]"},{"why":"Defines the JVFH lazy-language type system, including type syntax, the typing judgment, sharing and subtype relations, and most of the rules this paper adapts.","marker":"[9]"},{"why":"Supplies the mutual-recursion type rule and its soundness proof, which the paper turns into LETREC GC and then finds a counterexample to.","marker":"[10]"},{"why":"Is the master’s thesis containing the full implementation; this paper is a summary of it.","marker":"[12]"},{"why":"Documents the GHC CoreSyn syntax that the adapted rules are written against.","marker":"[1]"},{"why":"Documents the GHC plugin API used to extract Core from the compiler pipeline.","marker":"[3]"},{"why":"Represents the prior strict-language analysis for OCaml, the comparison point that motivates handling actual lazy code.","marker":"[6]"}],"fun_headline_variants":["Haskell cost analysis exposes unsound rule in type system","GHC Core adaptation reveals flaw in lazy-language resource logic","Type-based resource bounds now work on real Haskell code","Unsound LETREC rule found via GHC Core resource analysis"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the adapted typing rules soundly over-approximate the real cost of evaluating GHC Core expressions; the paper gives no operational semantics for Core and no soundness proof, so any rule that accidentally under-approximates (as LETREC did) breaks the upper-bound guarantee.","fun_headline_variants_meta":{"raw":{"variants":["Haskell cost analysis exposes unsound rule in type system","GHC Core adaptation reveals flaw in lazy-language resource logic","Type-based resource bounds now work on real Haskell code","Unsound LETREC rule found via GHC Core resource analysis"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000153,"raw_usage":{"total_tokens":1145,"prompt_tokens":818,"completion_tokens":327,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":434,"completion_tokens_details":{"reasoning_tokens":259}},"tokens_in":434,"tokens_out":327,"duration_ms":3761,"temperature":1.0,"reasoning_tokens":259,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:28:27.593728+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Instrument a compiled GHC Core program with an allocation counter, run the paper’s analysis on a set of mutually recursive infinite-list programs, and look for any case where the returned upper bound is below the measured allocation; the Fibonacci example shows exactly this failure mode, and the paper’s fix would be vindicated by finding no further such cases.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces the amortized analysis method with type-annotated potentials and LP-generated bounds that this line of work builds on."},{"cited_title":"Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen","cited_arxiv_id":null,"evidence_quote":"Supplies the mutual-recursion type rule and its soundness proof, which the paper turns into LETREC GC and then finds a counterexample to."},{"cited_title":"Master’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen","cited_arxiv_id":null,"evidence_quote":"Is the master’s thesis containing the full implementation; this paper is a summary of it."},{"cited_title":"https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/CoreSyn.html","cited_arxiv_id":null,"evidence_quote":"Documents the GHC CoreSyn syntax that the adapted rules are written against."},{"cited_title":"https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/Plugins.html","cited_arxiv_id":null,"evidence_quote":"Documents the GHC plugin API used to extract Core from the compiler pipeline."}],"review_version":1}