{"id":"cdee78f6-2545-4060-a37b-71802af67566","arxiv_id":"1908.07776","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A polarity-based construction plus a conjuring lemma yields free theorems as simple equations, implemented in a compact Haskell tool.","lead":"A simpler route to free theorems for polymorphic programs, built on a polarity-based transformation and a short proof from relational parametricity, produces clean equations instead of unwieldy logical formulas. The paper ships a compact Haskell generator, so the method is directly testable.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The unproved correctness of the mono recursion is the load-bearing gap: if the polarity bookkeeping is wrong for a nested type, the generated term cannot be fed to the conjuring lemma and the central equality is not established.","rationale":"The paper's central contribution is a deterministic generator for free theorems that avoids relational unfolding. The conjuring lemma (Lemma 1) is proved in a few lines, and the implementation is short and reproducible. The weakest point is indeed the step from the lemma to the generator: the term e = mono(σ) f must satisfy the lemma's hypotheses, which requires mono to have the claimed polarity behaviour. The paper does not prove this; it asserts that it is easy to see. This is not a demonstrated error—my own calculations for several types, including α→α, (α→α)→(α→α), and (α→Bool)→[α]→Maybeα, confirm that the recursion behaves as intended—but the absence of a proof is a genuine gap because the entire correctness of the generated equations rests on it. The simplifier exhaustiveness and Section 3.5's completeness criterion are secondary: they affect the quality or generality of the output, not its validity. I therefore agree with the reader that the appropriate verdict is CONDITIONAL, pending a proof of the mono typing/behaviour lemma. A structural induction is the decisive check; it either closes the gap or exposes a concrete type shape on which the construction fails.","tokens_in":14977,"tokens_out":33792,"duration_ms":314096,"concrete_test":"State and prove by structural induction on σ the typing lemma for mono: for all τ1, τ2, pre::τ1→α, post::α→τ2, the term mono_{pre,post}(σ) is well-typed as a function from σ to σ^, where σ^ is σ with every negative occurrence of α replaced by τ1 and every positive occurrence by τ2, and the swapped call in the σ1→σ2 case realizes the polarity flip. Check the base cases (α, Bool, Int), the covariant cases ([σ], Maybe σ), and the function case, including the direction of the swapped conversion. If the induction goes through, the mono concern is resolved; if it fails, the failing type shape is a concrete counterexample to the central construction.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 3.3 defines mono_{pre,post}(σ) by structural recursion, with pre/post swapped in contravariant positions, and then derives the free theorem as mono_{id,g}(σ) f = mono_{g,id}(σ) f. The paper explicitly states: \"We do not prove the general behaviour, but it should be easy to see that mono_{pre,post}(σ) does what we claim.\" This unproved behaviour is load-bearing: for the conjuring lemma to apply, e = mono_{pre,post}(σ) f must have a closed type, with negative α occurrences instantiated to τ1 and positive ones to τ2, and after substitution [id/pre, g/post] and [g/pre, id/post] both sides must be well-typed terms of the same closed type. If the swapped recursion makes an error in a deeply nested function type (e.g., a type like ((α→Int)→α)→α with several polarity flips), the generated term would be ill-typed or would instantiate α at the wrong type, so the equality would not follow from parametricity. The Haskell implementation type-checks on individual examples, but its Func type does not by itself enforce the polarity typing property, so the implementation is not a substitute for the missing proof.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":15205,"tokens_out":6549,"duration_ms":68173,"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":[{"comment":"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.","section":"Section 3.3"},{"comment":"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.","section":"Section 3.4"},{"comment":"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.","section":"Section 3.5"}],"minor_comments":[{"comment":"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.","section":"Section 3.4"},{"comment":"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.","section":"Section 4"},{"comment":"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.","section":"Figure 1"}],"recommendation":"major_revision","confidential_remarks":"The paper's central idea is attractive and the conjuring lemma is a useful reformulation. However, the unproved mono correctness is a genuine gap for a journal publication, and the eta-expansion issue in the simplifier could be a correctness problem in seq settings. Both appear fixable with additional proof and care. The paper is also somewhat informal in places; a revision should tighten the technical presentation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a nice, genuinely simpler way to derive free theorems, and the shipped Haskell generator makes it concrete. I would send it to a referee, but the load-bearing correctness claim for the mono construction is stated and not proved, and the author knows it.\n\nWhat is actually new: the conjuring lemma appeared before in the functional-logic setting, but this paper re-proves it from standard relational parametricity and then builds the mono recursion on top, giving deterministic simplification rules and a compact implementation. The payoff is real: instead of unfolding relational interpretations and fighting with higher-order logic, you get a simple equation between two lambda-terms. The examples in Section 2.4 make the improvement tangible, and the implementation is small enough to inspect and reuse. Credit is due for the clean presentation and for shipping code.\n\nSoft spots, in proportion: the main one is exactly what the author admits in Section 3.3: \"We do not prove the general behaviour, but it should be easy to see that mono_{pre,post}(σ) does what we claim.\" That is load-bearing. The conjuring lemma only applies if e = mono_{pre,post}(σ) f has the right closed type, with negative α instances replaced by τ1 and positive ones by τ2. The stress-test note about nested polarity flips is on point: for a type like ((α→Int)→α)→α, a small mistake in the recursive switching would make the whole construction ill-typed. I suspect the fix is a routine induction on σ, but the paper should give that argument rather than asking the reader to see it.\n\nThe other soft spot is Section 3.5: the criterion for when the method loses generality is explicitly conjectural. That is honest but means the paper's scope is not fully pinned down. The exhaustiveness of the simplifier is argued via the implementation's two syntax types rather than a formal statement; again, reasonable, but a bit lighter than I would like. None of these feel fatal. The core idea is simple enough that the missing proofs are probably short.\n\nCitation pattern looks appropriate. The self-citation to [10] is justified because that is where the conjuring lemma first appeared; the paper is clear about what is inherited and what is new.\n\nThis is a paper for people who implement or teach free theorems, and for PL researchers who want a low-ceremony bridge from parametricity to dinaturality. It deserves a serious referee, with the request that the mono correctness proof and the completeness criterion be properly stated.","headline":"A genuinely simple free-theorem generator built on a clean lemma; the main gap is an explicitly unproved correctness property of the central construction.","tokens_in":15706,"tokens_out":1592,"would_cite":true,"duration_ms":64937,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"One recursion turns any free theorem into a plain equation","keywords":["free theorems","relational parametricity","dinaturality","polarity","type-directed recursion","lambda calculus","Haskell","normalisation by evaluation"],"falsifier":"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.","tokens_in":14746,"feed_emoji":"📜","tokens_out":9630,"duration_ms":290415,"temperature":0.7,"pith_summary":"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.","feed_headline":"One recursion turns any free theorem into a plain equation","feed_subtitle":"A polarity-aware recursion replaces relation unfolding, giving compact unconditional equations in one deterministic pass.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines free theorems as the relational-parametricity consequence that f's instantiations are related; the standard derivation procedure this paper replaces.","marker":"[14]"},{"why":"Supplies the relational parametricity theorem that the conjuring lemma's proof is extracted from.","marker":"[12]"},{"why":"Previous statement of the conjuring lemma for a functional-logic language (Theorem 7.8 there), giving the lemma and its name.","marker":"[10]"},{"why":"Identifies dinaturality in polymorphic settings, which the generated equality $\\mathsf{mono}_{id,g}=\\mathsf{mono}_{g,id}$ is recognised as instantiating.","marker":"[5]"},{"why":"Establishes how free theorems change in the presence of seq, motivating the strictness/totality side conditions on g reused here.","marker":"[9]"},{"why":"Recent work exploiting the parametricity-dinaturality connection, providing context for why the categorical route is worth simplifying.","marker":"[8]"}],"fun_headline_variants":["One recursion turns free theorems into plain equations","Polarity-aware recursion simplifies free theorem derivation","Dinaturality via recursion: compact free theorems easily","Unconditional free theorems from a single deterministic pass","Free theorems without the tedious unfolding: one recursion"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["One recursion turns free theorems into plain equations","Polarity-aware recursion simplifies free theorem derivation","Dinaturality via recursion: compact free theorems easily","Unconditional free theorems from a single deterministic pass","Free theorems without the tedious unfolding: one recursion"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000251,"raw_usage":{"total_tokens":1583,"prompt_tokens":998,"completion_tokens":585,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":614,"completion_tokens_details":{"reasoning_tokens":514}},"tokens_in":614,"tokens_out":585,"duration_ms":6181,"temperature":1.0,"reasoning_tokens":514,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:56:16.808316+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"map\" (mono t pre post ) mono (Maybe t) pre post = Map","cited_arxiv_id":null,"evidence_quote":"Defines free theorems as the relational-parametricity consequence that f's instantiations are related; the standard derivation procedure this paper replaces."},{"cited_title":"In: Information Processing, Proceedings","cited_arxiv_id":null,"evidence_quote":"Supplies the relational parametricity theorem that the conjuring lemma's proof is extracted from."},{"cited_title":"In: Principles and Practice of Declarative Programming, Proceedings","cited_arxiv_id":null,"evidence_quote":"Previous statement of the conjuring lemma for a functional-logic language (Theorem 7.8 there), giving the lemma and its name."},{"cited_title":"Theo- retical Computer Science 70(1), 35–64 (1990)","cited_arxiv_id":null,"evidence_quote":"Identifies dinaturality in polymorphic settings, which the generated equality $\\mathsf{mono}_{id,g}=\\mathsf{mono}_{g,id}$ is recognised as instantiating."},{"cited_title":"In: Principles of Programming Languages, Proceedings","cited_arxiv_id":null,"evidence_quote":"Establishes how free theorems change in the presence of seq, motivating the strictness/totality side conditions on g reused here."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Recent work exploiting the parametricity-dinaturality connection, providing context for why the categorical route is worth simplifying."}],"review_version":1}