Pith. sign in

REVIEW 3 major objections 3 minor 14 references

Free Theorems Simply, via Dinaturality

T0 review · 3 major / 3 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 One recursion turns any free theorem into a plain equation

desk verdict A genuinely simple free-theorem generator built on a clean lemma; the main gap is an explicitly unproved correctness property of the central construction. read the letter →

arxiv 1908.07776 v1 pith:BSWVG553 submitted 2019-08-21 cs.PL

Janis Voigtländer This is my paper · ORCID
classification cs.PL
keywords freetheoremsrelationalparametricitydinaturalitypolaritytype-directedrecursionlambdacalculusHaskellnormalisationbyevaluation
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

This paper claims that free theorems for a function $f::\forall\alpha.\sigma$ can be generated by a deterministic structural recursion on $\sigma$, without unfolding the definitions of relational parametricity. The generated statement is always an unconditional equation between two $\lambda$-terms, obtained as $\mathsf{mono}_{id,g}(\sigma)\,f = \mathsf{mono}_{g,id}(\sigma)\,f$, where $\mathsf{mono}$ replaces negative occurrences of $\alpha$ through one bridge function and positive occurrences through another. A reader should care because this turns a tedious, heuristic-heavy derivation into a predictable half-page algorithm, and the same recursion works in language settings (partiality, seq, imprecise errors) where standard derivations need extra side conditions. If the construction is right, free theorems are exactly the dinaturality instances of the type, so the categorical content is recovered without category theory.

What carries the argument

The load-bearing object is the recursion $\mathsf{mono}_{pre,post}(\sigma)$, a type-directed term construction: at a type variable it emits $post$, at base types identity, at list/Maybe constructors it lifts via map/fmap, and at a function type $\sigma_1\to\sigma_2$ it produces $\lambda h.\,\mathsf{mono}_{pre,post}(\sigma_2)\circ h\circ\mathsf{mono}_{post,pre}(\sigma_1)$, swapping the bridge functions as polarity flips. It works together with the conjuring lemma (Lemma 1), which says that any closed-type term built with free $pre$ and $post$ obeys the equation after substituting $id$ and $g$ for them in the two possible ways. A secondary piece is the simplifier $\lfloor\cdot\rfloor$, whose exhaustive case analysis guarantees that all parts contributed by $\mathsf{mono}$ are reduced, so the final equation is compact and contains no residual compositions or identities.

What would settle it

Take the generator's definition of $\mathsf{mono}$ and type-check the term it builds for a systematically chosen set of type expressions, such as all types of size up to ten built from arrows, lists, and Maybe. A single type $\sigma$ for which $\mathsf{mono}_{pre,post}(\sigma)$ has a different type than the claimed one — for instance, where a positive occurrence is replaced by $pre$ instead of $post$, or a function composition is ill-typed — would invalidate the construction. Alternatively, instantiate the generated equality in a concrete model (e.g., with $f$ a known parametric function and $g$ a non-trivial strict map) and check whether the two sides are equal; since the paper gives no general proof of the recursion's behaviour, one counterexample to either check settles the matter.

Watch

Extended reading notes

Core claim

The paper's central claim is that every free theorem for a single-variable polymorphic function can be stated as $\mathsf{mono}_{id,g}(\sigma)\,f = \mathsf{mono}_{g,id}(\sigma)\,f$, where $\mathsf{mono}_{pre,post}(\sigma)$ is defined by recursion on the type: $\alpha\mapsto post$, base types to identity, datatypes via map/fmap, and $\sigma_1\to\sigma_2$ by $\lambda h.\,\mathsf{mono}_{pre,post}(\sigma_2)\circ h\circ\mathsf{mono}_{post,pre}(\sigma_1)$. The justification is the conjuring lemma: if $e$ is a closed-type term using $\alpha$ only internally with free variables $pre::\tau_1\to\alpha$ and $post::\alpha\to\tau_2$, then $e[\tau_1/\alpha, id/pre, g/post] = e[\tau_2/\alpha, g/pre, id/post]$ for any suitable $g::\tau_1\to\tau_2$. Plugging $e=\mathsf{mono}_{pre,post}(\sigma)\,f$ into the lemma gives the desired equality after substituting $id$ and $g$ for the bridge variables. The paper further claims that a small deterministic simplifier (inlining compositions, eliminating identities, $\beta$-reducing) turns the raw equality into a compact unconditional free theorem, and that a type loses this unconditional form only when it contains a negative subexpression in which both a positive and a negative $\alpha$ occur.

Load-bearing premise

The recursion's correctness is assumed rather than proven: the paper states, without proof, that $\mathsf{mono}_{pre,post}(\sigma)$ always produces a well-typed term of the intended closed type with negative $\alpha$ occurrences replaced via $pre$ and positive ones via $post$; if any type shape violates this, the generated equation is not a valid free theorem.

Editorial extensions

If this is right

  • Free theorems can be produced by a deterministic, terminating recursion; no search heuristics are needed, and the core generator is about half a page of code.
  • The same $\mathsf{mono}$ construction applies across language settings: with total functions, partial functions, seq, or imprecise error semantics, only the side condition on $g$ (strict, or strict and total) changes, not the derivation or simplification rules.
  • For types like $((([\alpha]\to Int)\to Int)\to Int)\to\alpha$, the generator yields a compact equation where previously available generators output a quantified precondition formula; the first is equivalent in eta-reasonable settings and simpler to read.
  • The equality $\mathsf{mono}_{id,g}(\sigma)\,f = \mathsf{mono}_{g,id}(\sigma)\,f$ is exactly a dinaturality condition, so the paper provides a direct route from relational parametricity to dinaturality without introducing categorical definitions.
  • When an unconditional equation necessarily loses generality — the paper's criterion is a negative subexpression containing both a positive and a negative $\alpha$, as in $(\alpha\to\alpha)\to\alpha\to\alpha$ — the generator still outputs a valid instance, just not the most general free theorem.

Reading between the lines

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

  • One likely extension is to types polymorphic in several variables: the same polarity-based recursion could run with a tuple of bridge functions per variable, and the conjuring lemma should generalize via simultaneous substitutions, though the paper does not spell this out.
  • Because the conjuring lemma does not depend on the exact relational action for datatypes, the generator core should be portable to new datatypes or to non-Haskell semantics as long as a parametricity theorem exists; this is a testable claim, not something the paper proves.
  • A formal proof of the typing property of $\mathsf{mono}$, and of the polarity criterion in Section 3.5, would turn the paper's 'easy to see' / 'we believe' statements into theorems; the provided implementation and the higher-order abstract syntax / normalisation-by-evaluation scaffolding make such a formalisation a concrete next step.
  • The simplification rules are designed to avoid eta-reduction in the presence of seq; an interesting stress test is to check whether the generated equations for arbitrary nesting depth never require an eta-reduction step to become valid, which would confirm the claimed uniformity.
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 / 3 minor

Summary. The paper proposes a method to generate free theorems for polymorphic functions directly from relational parametricity, avoiding the usual unfolding of relational actions. It introduces a "conjuring lemma" (Lemma 1) that turns parametricity into an equality condition on closed terms, and a structural recursion mono_{pre,post}(σ) that maps a type σ to a monomorphic type by replacing negative occurrences of α with τ1 via pre and positive ones with τ2 via post. For f :: ∀α.σ, the free theorem is generated as ⌊mono_{id,g}(σ) f⌋ = ⌊mono_{g,id}(σ) f⌋, where ⌊·⌋ is a deterministic simplifier. The paper claims this approach is simpler, more predictable, and more easily implemented than existing free-theorem generators, and it provides a compact Haskell implementation.

Significance. If correct, this work offers an elegant and deterministic route to free theorems, with potential pedagogical value and a small, reproducible implementation. The conjuring lemma is a clean restatement of parametricity that could simplify reasoning in several language settings. However, the central correctness of the mono recursion is asserted but not proved, and the simplifier's eta-expansion rule has a questionable justification in settings with seq and bottom. These gaps currently prevent full confidence in the main claims.

major comments (3)
  1. [Section 3.3] The correctness of the mono construction is load-bearing but unproved. The text states "We do not prove the general behaviour, but it should be easy to see that mono_{pre,post}(σ) does what we claim." For Lemma 1 to apply, the term e = mono_{pre,post}(σ) f must have a closed type, with negative occurrences of α instantiated to τ1 and positive ones to τ2. If the polarity bookkeeping fails in a nested type (e.g., with several function-arrow flips), the generated term could be ill-typed or could instantiate α at the wrong type, invalidating the derived equality. A structural induction proof on types is needed to justify the defining equations, especially the swap of pre and post in the σ1→σ2 case.
  2. [Section 3.4] The simplification function ⌊·⌋ is claimed to be semantics-preserving even in language settings with seq, where eta-reduction is invalid. The justification for the rule ⌊(λh→ body) t⌋ = λv→⌊ body[t/h] v⌋ relies on the assertion that f∘g = λv→ (f∘g) v is a valid equivalence in such settings. This is not generally true: if f∘g is ⊥, then seq distinguishes f∘g from λv→ (f∘g) v. Since the paper explicitly intends the method to work in the presence of seq (Section 2.3), this step needs either a precise argument showing why terms generated by mono never make the eta-expansion unsound, or a modification of the simplification rules to avoid the questionable expansion.
  3. [Section 3.5] The paper's criterion for when the approach loses generality is stated as "We believe it is an exact characterisation, but have no proof to show for it." This is a conjecture, not a theorem. Since the paper uses this criterion to explain when its output is weaker than the most general free theorem, it should either be proved or explicitly labelled as a conjecture, with the consequences of the uncertainty discussed.
minor comments (3)
  1. [Section 3.4] The grammar for the "Simple" class includes map and fmap, but the paper does not discuss how user-defined datatypes would be accommodated in the simplification rules. A sentence clarifying that the current implementation targets list and Maybe, with extension points for other datatypes, would help.
  2. [Section 4] The exhaustiveness argument for ⌊·⌋ is presented entirely through the Haskell implementation's type structure. It would be more accessible and more precise to state the syntactic characterization of mono-generated terms directly in the paper, independent of the implementation, and then argue exhaustiveness from that characterization.
  3. [Figure 1] The notation in the example calculation is sometimes dense, especially the steps involving nested ⌊·⌋. Consider adding brief annotations or line-by-line explanations to improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity is present: the free-theorem equality is a direct instance of the conjuring lemma, which is re-proved here from relational parametricity, and the unproved mono correctness is a correctness gap rather than circularity.

full rationale

The load-bearing derivation chain is: relational parametricity (Theorem 1, external), Lemma 1 as a proved corollary, and then the generated theorem monoid,g(σ) f = monog,id(σ) f as an instance of Lemma 1 with e = monopre,post(σ) f. Lemma 1 is not assumed from the cited prior work; Section 3.2 contains a proof from Theorem 1 via graph relations, so the self-citation is non-load-bearing. The final equality follows by the paper's own substitution observations: monopre,post(σ)[id/pre,g/post] = monoid,g(σ) and monopre,post(σ)[g/pre,id/post] = monog,id(σ); this is a syntactic instance of a parametricity corollary, not a fitted or renamed input. The only load-bearing unproved claim is the correctness of mono's polarity bookkeeping: Section 3.3 says 'We do not prove the general behaviour, but it should be easy to see that monopre,post(σ) does what we claim.' If mono failed for some nested type, the premise e :: τ with closed type would fail and Lemma 1 would not apply. That is a proof or completeness gap in the algorithm, but it is not circular: the conclusion is not assumed in the premise, and the paper offers a concrete construction whose type-correctness is independently checkable. Similarly, the 'exact characterisation' conjecture in Section 3.5 is admittedly unproved ('We believe it is an exact characterisation, but have no proof'), but that is an uncertainty about the criterion's generality, not a circular definition. No equation in the paper reduces by construction to its own input, and no prediction is statistically forced by fitted data.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper relies on the standard relational parametricity theorem and standard properties of the relational interpretation; these are external to the paper. The only paper-specific unproved assumption is the general correctness of the mono construction and the simplification engine's exhaustiveness. No free parameters are fitted to data, and no new entities are postulated.

assumptions (5)
  • domain assumption Relational parametricity holds for the considered language setting (Theorem 1).
    Invoked in the proof of the conjuring lemma (Sections 3.1 and 3.2). Cited to Reynolds and Wadler, not proved in the paper.
  • standard math For any closed type τ, Δ_{∅,τ} is the identity relation.
    Used at the end of the conjuring lemma proof to turn relatedness into equality; stated in Section 3.1.
  • domain assumption The graph of a strict (and total, for seq) function is an admissible relation for parametricity.
    Needed to instantiate the relation variable R in the conjuring lemma proof; stated in Lemma 1.
  • ad hoc to paper The mono recursion correctly implements polarity-based type substitution.
    Section 3.3 says 'We do not prove the general behaviour, but it should be easy to see'. This unproved step is load-bearing for the method.
  • ad hoc to paper The simplification function preserves semantic equivalence and is exhaustive on mono output.
    Section 3.4 gives semantic arguments; Section 4 defers exhaustiveness to the implementation's types. No formal proof is given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Free Theorems Simply, via Dinaturality." pith.science (2026). https://pith.science/paper/BSWVG553

@misc{pith2026190807776,
  author       = {Pith},
  title        = {Pith review of: Free Theorems Simply, via Dinaturality},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BSWVG553}},
  note         = {Machine review of arXiv:1908.07776}
}
read the original abstract

Free theorems are a popular tool in reasoning about parametrically polymorphic code. They are also of instructive use in teaching. Their derivation, though, can be tedious, as it involves unfolding a lot of definitions, then hoping to be able to simplify the resulting logical formula to something nice and short. Even in a mechanised generator it is not easy to get the right heuristics in place to achieve good outcomes. Dinaturality is a categorical abstraction that captures many instances of free theorems. Arguably, its origins are more conceptually involved to explain, though, and generating useful statements from it also has its pitfalls. We present a simple approach for obtaining dinaturality-related free theorems from the standard formulation of relational parametricity in a rather direct way. It is conceptually appealing and easy to control and implement, as the provided Haskell code shows.

Figures

Figures reproduced from arXiv: 1908.07776 by the authors.

Figure 1
Figure 1. An example calculation, for bmonoid,g ((α → Bool) → [α] → Maybe α) f c Another issue is the unsatisfactory “simplification” of fmap g to fmap (λv3 → g v3) in [PITH_FULL_IMAGE:figures/full_fig_p014_1.png] view at source ↗
Figure 2
Figure 2. module Generate, generation and simplification of free theorems [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗
Figure 3
Figure 3. module Syntax, datatypes for types and different forms of (higher-order abstract syntax) terms, and eta-reduction [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: module Main, putting the generator together with input and output [PITH_FULL_IMAGE:figures/full_fig_p019_4.png]
Figure 5
Figure 5. Figure 5: An example session [PITH_FULL_IMAGE:figures/full_fig_p020_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [10]

    In: Principles and Practice of Declarative Programming, Proceedings

    Mehner, S., Seidel, D., Straßburger, L., Voigtl¨ ander, J.: Parametricity and prov- ing free theorems for functional-logic languages. In: Principles and Practice of Declarative Programming, Proceedings. pp. 19–30. ACM Press (2014)

    work page 2014

  2. [1]

    http://hackage.haskell.org/package/free-theorems, accessed: August 2019

    work page 2019

  3. [2]

    http://free-theorems.nomeata.de, accessed: August 2019

    work page 2019

  4. [3]

    http://hackage.haskell.org/package/lambdabot, accessed: August 2019

    work page 2019

  5. [4]

    http://hackage.haskell.org/package/ft-generator, accessed: August 2019

    work page 2019

  6. [5]

    Theo- retical Computer Science 70(1), 35–64 (1990)

    Bainbridge, E., Freyd, P., Scedrov, A., Scott, P.: Functorial polymorphism. Theo- retical Computer Science 70(1), 35–64 (1990)

    work page 1990

  7. [6]

    In: Logic in Computer Science, Proceedings

    Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: Logic in Computer Science, Proceedings. pp. 203–211. IEEE Press (1991)

    work page 1991

  8. [7]

    In: Func- tional Programming Languages and Computer Architecture, Proceedings

    Gill, A., Launchbury, J., Peyton Jones, S.: A short cut to deforestation. In: Func- tional Programming Languages and Computer Architecture, Proceedings. pp. 223–

    work page

Show all 14 references
  1. [8]

    Hackett, J., Hutton, G.: Programs for cheap! In: Logic in Computer Science, Proceedings. pp. 115–126. IEEE Press (2015)

    2015

  2. [9]

    In: Principles of Programming Languages, Proceedings

    Johann, P., Voigtl¨ ander, J.: Free theorems in the presence of seq. In: Principles of Programming Languages, Proceedings. pp. 99–110. ACM Press (2004)

    2004

  3. [11]

    In: Programming Language Design and Implementation, Proceedings

    Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Programming Language Design and Implementation, Proceedings. pp. 199–208. ACM Press (1988)

    1988

  4. [12]

    In: Information Processing, Proceedings

    Reynolds, J.: Types, abstraction and parametric polymorphism. In: Information Processing, Proceedings. pp. 513–523. Elsevier (1983)

    1983

  5. [13]

    In: Typed Lambda Calculi and Applications, Proceedings

    Stenger, F., Voigtl¨ ander, J.: Parametricity for Haskell with imprecise error semantics. In: Typed Lambda Calculi and Applications, Proceedings. LNCS, vol. 5608, pp. 294–308. Springer-Verlag (2009)

    2009

  6. [14]

    map" (mono t pre post ) mono (Maybe t) pre post = Map

    Wadler, P.: Theorems for free! In: Functional Programming Languages and Com- puter Architecture, Proceedings. pp. 347–359. ACM Press (1989) Free Theorems Simply, via Dinaturality 17 A Implementation See Section 4 for some explanation of the implementation. To run the genera- t...

    1989

Pith tools

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