Pith. sign in

REVIEW 3 major objections 4 minor 15 references

Type-Based Resource Analysis on Haskell

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 1908.06478 v1 pith:3Z7JGJ6V submitted 2019-08-14 cs.PL

Franz Siglmüller (Ludwig Maximilian University of Munich) This is my paper · ORCID
classification cs.PL
keywords amortizedanalysisresourceboundsHaskellGHCCoretype-basedcostlazyevaluationlinearprogrammingcompilerplugin
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

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.

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 (3)
  1. [Abstract; Section 8] 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.
  2. [Section 5, LETREC GC rule] 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.
  3. [Section 4, Type syntax workarounds] 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.
minor comments (4)
  1. [Figure 5, CONS GC rule] 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.
  2. [Section 3] 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.
  3. [Section 4] 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.
  4. [Section 6] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the derived resource bounds are LP solutions from stated typing rules, not fitted or self-referential predictions.

full rationale

The paper's derivation chain is: GHC Core is translated to a simplified representation; JVFH-style typing rules adapted for Core produce linear constraints; an LP solver computes annotated types representing resource bounds. No step re-inserts the claimed output as an input. The cost constants are user-set parameters, the adapted rules are concretely stated in Figures 4-7, and the reused JVFH relations are external prior work rather than outputs of this paper. The evaluation against the JVFH demo is a sanity comparison, not calibration: the paper explicitly notes that annotations may differ because 'the LP solver also has some freedom in how values are assigned to variables'. Section 8's admission that soundness of the adapted type system is unproven, and the Section 5/7 LETREC GC counterexample, are correctness gaps rather than circularity: an unsound rule can yield wrong bounds, but the bounds are not defined as whatever the rules happen to produce. There is no fitted input renamed as a prediction, and the only self-citation (the author's master's thesis [12]) is provenance, not load-bearing.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The tool's contributions are contingent on several unproven assumptions: the soundness of reused JVFH rules, the fidelity of the GHC Core cost model, the validity of the polymorphism workaround, and the correctness of hard-coded primitive operations. The paper explicitly notes the lack of a soundness proof, making these axioms the main risk to the central claim.

free parameters (1)
  • Cost model constants (Kvar, Kapp, Kcons, Klet, Kmatch, Kletrec, Kprim) = user-defined
    The analysis returns bounds as linear functions of these user-set constants; the paper gives no operational grounding for their values, only that they correspond to the chosen cost model (allocations or time).
assumptions (4)
  • domain assumption Soundness of the reused JVFH type rules (structural rules, Sharing, subtype) transfers to the adapted system.
    Section 5 states many rules are reused without modification; the paper relies on their correctness but found one counterexample in LETREC (Section 7), so this transfer is not established.
  • domain assumption GHC Core cost semantics are adequately modeled by the typing rules, i.e., evaluation to weak head normal form with thunk costs matches the system's resource accounting.
    The paper analyzes optimized GHC Core (Section 3) and assumes it reflects runtime costs, but no operational semantics for Core is given to justify the cost annotations.
  • ad hoc to paper Polymorphic functions can be treated as monomorphic by ignoring type abstractions and applications via the artificial function type.
    Section 5, rules TYABS GC and TYAPP GC; the paper admits this only works for monomorphic uses, otherwise unification fails or types contain free variables.
  • domain assumption Hard-coded primitive operations and Prelude variables are costed correctly with constant Kprim and inlined by GHC when needed.
    Section 6; there is no multi-module support, so correctness depends on inlining and on a single cost constant for all primitive operations.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Type-Based Resource Analysis on Haskell." pith.science (2026). https://pith.science/paper/3Z7JGJ6V

@misc{pith2026190806478,
  author       = {Pith},
  title        = {Pith review of: Type-Based Resource Analysis on Haskell},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3Z7JGJ6V}},
  note         = {Machine review of arXiv:1908.06478}
}
read the original abstract

We propose an amortized analysis that approximates the resource usage of a Haskell expression. Using the plugin API of GHC, we convert the Haskell code into a simplified representation called GHC Core. We then apply a type-based system which derives linear upper bounds on the resource usage. This setup allows us to analyze actual Haskell code, whereas previous implementations of similar analyses do not support any commonly used lazy functional programming languages.

Figures

Figures reproduced from arXiv: 1908.06478 by the authors.

Figure 1
Figure 1. The original Haskell code is first parsed into an abs [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Simplified representation of the GHC Core syntax [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 4
Figure 4. Unmodified syntax driven type rules However, LETRECGC is also noteworthy as it is the only inference rule in our adapted type system that makes use of the ⊳ operator. There exists a soundness proof of this rule [10], indicating that the usage of this operator should be correct; But during our tests, we encountered a counter-example where this rule does allow for under-approximation: letrec zipWith = ··· in let one =… view at source ↗
Figures from the paper (4 more)
Figure 5
Figure 5. Figure 5: Modified type rules M ⊂ {ci(xi) → ei} n i=1 ∪ {default → ed} |Ai | = |xi | B = µX.{ci : (qi ,Ai)} n i=1 Γ p p ′ e0 : B ∆, xi :Ai [X 7→ B], y:T 0 (B) p ′ +qi p ′′ ei :C for all i, if (ci(xi) → ei) ∈ M ∆, y:T 0 (B) p ′ +qi p ′′ ed :C for all i, if (ci(xi) → ei) ∈/ M and …
Figure 6
Figure 6. Figure 6: Adapted type rules for case expressions structure allocation via a letcons expression, which fulfills multiple purposes at once: First, it fully applies the constructor to all of its arguments; This is simple, because all arguments have to be variables, so this can be …
Figure 7
Figure 7. Figure 7: New type rules for handling type expressions [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 8
Figure 8. Figure 8: Outline of the architecture of our analysis [PITH_FULL_IMAGE:figures/full_fig_p010_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 10 canonical work pages

  1. [1]

    https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/CoreSyn.html

    The GHC API: CoreSyn . https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/CoreSyn.html. Accessed: 2019-04-29

    work page 2019

  2. [2]

    https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/HsExpr.html

    The GHC API: HsExpr . https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/HsExpr.html. Accessed: 2019-04-29

    work page 2019

  3. [3]

    https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/Plugins.html

    The GHC API: Plugins . https://downloads.haskell.org/~ghc/8.2.2/docs/html/ libraries/ghc-8.2.2/Plugins.html. Accessed: 2019-04-29

    work page 2019

  4. [4]

    https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/ generated-code?version_id=33352ae3

    Max Bolingbroke et al.: The GHC Commentary: I know kung fu: learning STG by example . https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/ generated-code?version_id=33352ae3. Accessed: 2019-04-29

    work page 2019

  5. [5]

    In: 24rd Interna- tional Conference on Computer Aided V erification (CA V’12) , Lecture Notes in Computer Science 7358, Springer, pp

    Jan Hoffmann, Klaus Aehlig & Martin Hofmann (2012): Resource Aware ML . In: 24rd Interna- tional Conference on Computer Aided V erification (CA V’12) , Lecture Notes in Computer Science 7358, Springer, pp. 781–786, doi: 10.1007/978-3-642-31424-7_64

    doi:10.1007/978-3-642-31424-7_64 2012

  6. [6]

    In: ACM SIGPLAN Notices , 52, ACM, pp

    Jan Hoffmann, Ankush Das & Shu-Chun Weng (2017): Towards Automatic Resource Bound Anal- ysis for OCaml . In: ACM SIGPLAN Notices , 52, ACM, pp. 359–373, doi: 10.1145/3009837. 3009842

    doi:10.1145/3009837 2017

  7. [7]

    Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    Nataliya Irkha (2016): Evaluation und Erweiterung einer Typ-basierten Kostenana lyse f ¨ur funk- tionale Sprachen mit verz ¨ogerter Auswertung. Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    work page 2016

  8. [8]

    Steffen Jost (2010): Automated Amortised Analysis. Ph.D. thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    work page 2010

Show all 15 references
  1. [9]

    Journal of Automated Reasoning 59(1), pp

    Steffen Jost, Pedro V asconcelos, M´ ario Florido & Kevin Hammond (2017): Type-Based Cost Analysis for Lazy Functional Languages . Journal of Automated Reasoning 59(1), pp. 87– 120, doi: 10.1007/s10817-016-9398-9 . Available at http://www.dcc.fc.up.pt/~pbv/ research/JAR2016-draft.pdf

    2017 doi

  2. [10]

    Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    Sophie Kleber (2017): Mutual Recursive Definitions for a Type-Based Cost Analysis for Lazy Func- tional Languages. Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    2017

  3. [11]

    Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    Maksym Redka (2017): Erweiterung des Prototyps einer Typ-basierten Kostenanal yse f ¨ur funk- tionale Sprachen mit verz ¨ogerter Auswertung. Bachelor’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    2017

  4. [12]

    Master’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    Franz Siglm¨ uller (2018): Implementation of an Automated Amortized Analysis on GHC Co re as Compiler Plugin. Master’s thesis, Ludwig-Maximilian-Universit¨ at M¨ unchen

    2018

  5. [13]

    In: ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI’07) , pp

    Martin Sulzmann, Manuel Chakravarty, Simon Peyton Jon es & Kevin Donnelly (2007): System F with Type Equality Coercions. In: ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI’07) , pp. 53–66, doi: 10.1145/1190315.1190324

    2007

  6. [14]

    https://downloads

    GHC Team (2017): GHC User’s Guide Documentation: Release 8.2.2 . https://downloads. haskell.org/~ghc/8.2.2/docs/users_guide.pdf

    2017

  7. [15]

    An- nals of Pure and Applied Logic 98(1-3), pp

    Joe B Wells (1999): Typability and type checking in System F are equivalent and u ndecidable. An- nals of Pure and Applied Logic 98(1-3), pp. 111–156, doi: 10.1016/S0168-0072(98)00047-5

    1999 doi

Pith tools

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