pith. machine review for the scientific record. sign in

arxiv: 2604.21467 · v1 · submitted 2026-04-23 · 💻 cs.PL

Recognition: unknown

Linear Constraints

Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg

Pith reviewed 2026-05-08 12:54 UTC · model grok-4.3

classification 💻 cs.PL
keywords linear constraintslinear typesHaskellqualified typesconstraint solvingtype inferenceresource managementGHC
0
0 comments X

The pith

Linear constraints act as implicit linear arguments in Haskell that the compiler fills automatically.

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

The paper introduces linear constraints as the linear counterpart to Haskell's class constraints. These allow programmers to control resources such as file handles and memory using linear types without writing explicit linear arguments each time. The authors present the feature as a qualified type system along with an inference algorithm that extends GHC's existing constraint solver. Soundness follows from a desugaring translation into Linear Haskell. If the approach holds, it makes safe resource management practical by cutting down on the boilerplate that explicit linear typing usually demands.

Core claim

Linear constraints are the linear counterpart of Haskell's class constraints. A linear constraint acts as an implicit linear argument that can be filled in automatically by the compiler. We present this new feature as a qualified type system, together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell. This paper is a revised and extended version that simplifies the formal system and solver while describing additional applications.

What carries the argument

The linear constraint, an implicit linear argument resolved automatically inside a qualified type system by an extended GHC constraint solver.

If this is right

  • Programmers gain safer resource handling with far less explicit linear argument code.
  • The inference algorithm integrates directly with GHC's current constraint solver.
  • Soundness is preserved for all programs through the desugaring to Linear Haskell.
  • Additional applications become feasible in areas such as memory management and file handling.
  • The simplified formal system supports easier implementation and extension.

Where Pith is reading between the lines

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

  • The same pattern of implicit linear arguments via qualified types could be ported to other languages with linear or affine type systems to lower annotation cost.
  • It opens a route to treating other resource-like effects as implicit constraints rather than explicit parameters.
  • Large-scale adoption would allow empirical measurement of how often linear constraints are inferred versus written out by hand.
  • Combining linear constraints with dependent types could yield protocols that track resource state more precisely at the type level.

Load-bearing premise

The desugaring translation from linear constraints to Linear Haskell faithfully preserves linearity and typing, and the extended constraint solver correctly implements the qualified type system without introducing unsoundness or incompleteness.

What would settle it

A concrete program using a linear constraint that the solver accepts but whose desugaring to Linear Haskell is ill-typed, or a program the solver rejects that should be accepted under the qualified type rules.

Figures

Figures reproduced from arXiv: 2604.21467 by Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg.

Figure 1
Figure 1. Figure 1: Interfaces for mutable arrays These capabilities exist at the type level and must refer to a specific array. To achieve this, an array arr of values of type a is tagged with a type variable n: arr :: MArray a n Then, the constraints Read n and Write n become evidence that the array can be read from or written to. As a convenience we also have a synonym for their product: type RW n = (Read n, Write n) That … view at source ↗
Figure 2
Figure 2. Figure 2: Interface for the built-in Linearly constraint Now, when new k (𝜆arr → p) is called, the RW n constraint is made available to the computation p that is provided unrestricted access to the new array arr of size k. 3.4 Linear Contexts with Linearly Working within a linear context provided using a continuation-based interface restricts the scope within which the bound variable can occur. Thus, when multiple r… view at source ↗
Figure 3
Figure 3. Figure 3: Division of the inputs of the w function when p is larger than q. That is, p = (a, x, b) and n = (y,z). If its input is small enough, then there is nothing to do for v, but otherwise it splits n into two new triangular matrices a and b and the top-right matrix x. (The bottom left is always empty.) The read-write ownership is transferred to each of the components. After recursively computing the closure of … view at source ↗
Figure 4
Figure 4. Figure 4: Nested array api (Ur m′ ,release top) ← fullSlice m (Ur m′′ ,release top deep) ← borrowDeep m′ fullSlice (Ur (t, b),release slices) ← sliceDeep m′′ (𝜆col → slice col row num) Linearly.return ( Ur (SliceMatrix t, SliceMatrix b), Linearly.do { release slices;release top deep;release top}) sliceMatrixV (SliceMatrix m) row num = Linearly.do (Ur (t, b),release slices) ← sliceDeep m (𝜆col → slice col row num) Li… view at source ↗
Figure 5
Figure 5. Figure 5: Requirements for the entailment relation view at source ↗
Figure 6
Figure 6. Figure 6: Grammar of the qualified type system Definition 5.4 (Entailment relation). The qualified type system is parameterised by a relation Q1 ⊩ Q2 between two simple constraints, as well as by a distinguished set D of duplicable atomic constraints. We write, abusing notation, Q ∈ D for a simple constraint Q = (U, L) if for all q ∈ L we have q ∈ D. (This isn’t a plain inclusion because L is a multiset and D.) The … view at source ↗
Figure 7
Figure 7. Figure 7: Qualified type system in section 7; the main difference is that Γ is addressed explicitly, whereas Q is used implicitly in rule E-Var. Because constraints are used implicitly, if there are several instances of the same q, it is non-deterministic which one is used in which instance of E-Var. How do we reconcile this non-determinism with the use of linear constraints, in section 4 to thread mutations? We cer… view at source ↗
Figure 8
Figure 8. Figure 8: Wanted-constraint entailment case:    𝜋·(𝐶1 ⊗ 𝐶2) = 𝜋·𝐶1 ⊗ 𝜋·𝐶2 1·(𝐶1 &𝐶2) = 𝐶1 &𝐶2 𝜔·(𝐶1 &𝐶2) = 𝜔·𝐶1 ⊗ 𝜔·𝐶2 𝜋·(𝜌·(Q =◦𝐶)) = (𝜋·𝜌)·(Q =◦𝐶) For the most part, scaling of wanted constraints is straightforward. The only peculiar case is when we scale the additive conjunction 𝐶1 &𝐶2 by 𝜔, the result is a multiplicative conjunction. The intuition here is that when if we have both 𝜔·𝐶1 and 𝜔·𝐶2, then … view at source ↗
Figure 9
Figure 9. Figure 9: Constraint generation Case expressions. Note the use of & in the conclusion of rule G-Case. We require that each branch of a case expression use the exact same (linear) assumptions; this is enforced by combining the emitted constraints with &, not ⊗. This can also be understood in terms of the array example of section 1: if an array is freed in one branch of a case, we require it to be freed (or frozen) in… view at source ↗
Figure 10
Figure 10. Figure 10: Concrete constraint entailment The key property of the constraint-generation algorithm is that, if the generated constraint is solvable, then we can indeed type the term in the qualified type system of section 5. That is, these rules are simply an implementation of our declarative qualified type system. Lemma 6.4 (Soundness of constraint generation). For all Qg, if Γ ⊢▶ e : 𝜏 { 𝐶 and Qg ⊢ 𝐶 then Qg; Γ ⊢ e… view at source ↗
Figure 11
Figure 11. Figure 11: Constraint solver Lemma 6.5 (Constraint solver soundness). If ⊢s 𝐶 { Q, then Q ⊢ 𝐶 Building on this atomic-constraint solver, we use a linear proof search algorithm based on the recipe given by Cervesato et al. (2000), with one caveat that we discuss in section 9.4 view at source ↗
Figure 12
Figure 12. Figure 12: Core calculus (subset) 7 Desugaring The semantics of our language is given by desugaring it into a simpler core language: a variant of the 𝜆 𝑞 calculus (Bernardy et al. 2017). We define the core language’s type system here; its operational semantics is the same, mutatis mutandis, as that of Linear Haskell. 7.1 The Core Calculus The core calculus is a variant of the type system defined in section 5, but wi… view at source ↗
Figure 13
Figure 13. Figure 13: Evidence passing and desugaring the definition. We present some of the interesting cases in fig. 13b, the complete definition of desugaring can be found in section A. The cases correspond to the E-Var, E-Unpack9 , and E-Sub rules, respectively. Variables are stored with qualified types in the environment, so they get translated to functions that take the evidence as argument. Accordingly, the evidence is … view at source ↗
Figure 14
Figure 14. Figure 14: Desugaring view at source ↗
read the original abstract

Linear constraints are the linear counterpart of Haskell's class constraints. Linearly typed parameters allow the programmer to control resources such as file handles and manually managed memory as linear arguments. Indeed, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. Linear constraints address this shortcoming: a linear constraint acts as an implicit linear argument that can be filled in automatically by the compiler. We present this new feature as a qualified type system, together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell. This paper is a revised and extended version of a previous paper by the same authors (arXiv:2103.06127). The formal system and the constraint solver have been significantly simplified and numerous additional applications are described.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper introduces linear constraints as the linear counterpart to Haskell's class constraints, acting as implicit linear arguments that the compiler fills automatically. It presents the feature via a qualified type system and an inference algorithm extending GHC's existing constraint solver. Soundness is claimed to follow from desugaring into Linear Haskell. The work is a revised and extended version of an earlier paper (arXiv:2103.06127), with a simplified formal system and solver plus additional applications.

Significance. If the desugaring translation can be shown to be faithful (preserving well-typedness and linearity) and the extended solver proven to accept precisely the programs whose desugared forms are valid in Linear Haskell, the result would be significant for practical linear typing in Haskell. It reduces the explicit-argument bureaucracy that currently limits adoption of Linear Haskell for resource management (e.g., file handles, manual memory). The simplifications relative to the prior version are a clear improvement in presentation.

major comments (2)
  1. Abstract: the sole justification offered for soundness is that 'linear constraints desugar into Linear Haskell,' yet the manuscript supplies no formal desugaring translation, no statement of the translation's faithfulness properties, and no proof sketch or correspondence argument. This is load-bearing for the central soundness claim; without it, the qualified type system and solver extension cannot be verified to be sound.
  2. Qualified type system and inference algorithm sections: the paper describes the type system and the extension to GHC's constraint solver at a high level but provides neither the concrete typing rules for linear constraints nor the precise solver rules for how implicit linear arguments are generated and discharged. Without these, it is impossible to check whether the solver correctly implements the type system or whether it could accept programs that desugar to ill-typed Linear Haskell terms (e.g., in the presence of polymorphism or interaction with existing constraints).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thoughtful review and for identifying areas where the presentation of our soundness argument and formal details could be strengthened. We address each major comment below and will incorporate revisions to improve clarity and rigor.

read point-by-point responses

  1. Referee: Abstract: the sole justification offered for soundness is that 'linear constraints desugar into Linear Haskell,' yet the manuscript supplies no formal desugaring translation, no statement of the translation's faithfulness properties, and no proof sketch or correspondence argument. This is load-bearing for the central soundness claim; without it, the qualified type system and solver extension cannot be verified to be sound.

    Authors: We agree that the abstract's reference to desugaring would be more robust with an explicit pointer to the supporting argument. The body of the paper (Section 5) provides a high-level description of the desugaring from linear constraints to explicit linear arguments in Linear Haskell, together with an informal argument that well-typedness and linearity are preserved. To make this load-bearing claim fully verifiable, we will add a dedicated subsection that states the desugaring translation formally, lists the faithfulness properties (preservation of typing judgments and linearity), and includes a concise proof sketch of the correspondence between the qualified type system and Linear Haskell. This revision will directly address the referee's concern while preserving the paper's focus on the practical extension to GHC. revision: yes

  2. Referee: Qualified type system and inference algorithm sections: the paper describes the type system and the extension to GHC's constraint solver at a high level but provides neither the concrete typing rules for linear constraints nor the precise solver rules for how implicit linear arguments are generated and discharged. Without these, it is impossible to check whether the solver correctly implements the type system or whether it could accept programs that desugar to ill-typed Linear Haskell terms (e.g., in the presence of polymorphism or interaction with existing constraints).

    Authors: The manuscript presents the qualified type system in Section 3 and the solver extension in Section 4, including the mechanisms by which linear constraints are treated as implicit linear arguments and how they interact with GHC's existing constraint solver. We acknowledge, however, that the presentation remains somewhat high-level to keep the exposition accessible. In the revision we will insert the concrete typing rules (including the introduction and elimination rules for linear constraints) and the precise solver rules that govern the generation and discharge of implicit linear arguments. These additions will explicitly cover interactions with polymorphism and other constraints, enabling readers to verify that the solver accepts precisely the programs whose desugared forms are valid in Linear Haskell. revision: yes

Circularity Check

0 steps flagged

Soundness grounded externally via desugaring to Linear Haskell; only minor self-citation to prior version

full rationale

The paper's central soundness claim rests on the statement that linear constraints desugar into Linear Haskell, an independent prior system. The note that this is a revised version of arXiv:2103.06127 constitutes a self-citation, but it is not load-bearing for the soundness argument. No derivation step reduces by construction to its own inputs, no fitted parameter is relabeled as a prediction, and no uniqueness theorem or ansatz is imported solely via self-citation. The qualified type system and extended solver are presented with an external anchor, satisfying the criteria for a low circularity score.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that Linear Haskell is sound and that the desugaring translation preserves that soundness. No free parameters or invented entities are introduced in the abstract description.

axioms (1)
  • domain assumption Linear Haskell is a sound linear type system
    Soundness of the new feature is delegated entirely to desugaring into this prior system.

pith-pipeline@v0.9.0 · 5449 in / 1242 out tokens · 57396 ms · 2026-05-08T12:54:36.939349+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

5 extracted references

  1. [1]

    5) Q1 ⊗Q 2 ⊩𝜋·Q 1 ⊗𝜋·Q 2 as required

    by C-Tensor Q′ 1 ⊗Q ′ 2 ⊢𝐶 1 ⊗𝐶 2 and by tensoring of the entailment relation (fig. 5) Q1 ⊗Q 2 ⊩𝜋·Q 1 ⊗𝜋·Q 2 as required. C-With We have that𝜋=1 since 𝐶1 &𝐶 2 is not in the image of scaling by𝜔. Therefore we can chooseQ ′ =Qand the result holds trivially. C-Impl In the conclusion of the rule,Qis already of the form 𝜋·Q′, so the result holds trivially □ Le...

  2. [2]

    ⊗1·q By induction hypothesis, Q′ 1 ∧Q ′ 2 ⊩Q ′ 1 and Q′ 1 ∧Q ′ 2 ⊩Q ′

  3. [3]

    5, gives (Q′ 1 ∧Q ′

    Which, tensoring with 1·q according to the rules of fig. 5, gives (Q′ 1 ∧Q ′

  4. [4]

    ⊗1·q⊩Q ′ 1 ⊗1·q and (Q′ 1 ∧Q ′

  5. [5]

    We conclude by definition ofQ 1 ∧Q 2

    ⊗1·q⊩Q ′ 2 ⊗1·q. We conclude by definition ofQ 1 ∧Q 2. Inf-DiffLandInf-DiffR These two cases are symmetric, so we’ll prove the case of Inf-DiffL,Inf-DiffLis similar. That is we have •Q 1 =(U 1,L 1 ⊎q)=Q ′ 1 ⊗1·q •Q 1 ∧Q 2 =(Q ′ 1 ∧Q 2) ⊗𝜔·q By induction hypothesisQ′ 1 ∧Q 2 ⊩Q ′ 1 and Q′ 1 ∧Q 2 ⊩Q 2. Now (Q′ 1 ∧Q 2) ⊗𝜔·q⊩ Q2 by the weakening rule of fig. 5...