One Weird Trick to Untie Landin's Knot

Paulette Koronkevich; William J. Bowman

REVIEW 4 major objections 5 minor 11 references

One Weird Trick to Untie Landin's Knot

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read This paper argues that higher-order references can be added to terminating languages if the type of a function's environment is kept predicative, and offers a universe-level rule for references that blocks Landin's Knot.

desk verdict A plausible and genuinely new diagnosis of Landin's Knot, wrapped in a conjecture that is honestly labeled as unproved; worth reading for the reframing, not for a theorem. read the letter →

arxiv 2507.21317 v1 pith:IPMITHK7 submitted 2025-07-28 cs.PL

Paulette Koronkevich , William J. Bowman This is my paper · ORCID

classification cs.PL

keywords Landin'sKnothigher-orderreferencesstrongnormalizationclosureconversionimpredicativequantificationpredicativityuniverselevelstermination

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 argues that adding mutable references that can store functions to a terminating language does not by itself create non-termination. The real culprit is the implicit impredicative quantification over a function's environment: through closure conversion, the classic Landin's Knot becomes a well-typed backpatch because a closure's environment type can be any type, including a reference to the closure itself. The authors propose a type-level fix in which a reference type Ref A lives one universe above the type it stores, so a closure cannot capture a reference to its own type, and they conjecture this restores strong normalization without linear types. An appendix derivation shows their rule makes the closure-converted Landin's Knot ill-typed; the termination conjecture itself is left unproved.

What carries the argument

The analytical device is closure conversion: functions are rewritten as explicit pairs of closed code and environment, typed as existential pairs such as ∃α:Type_j.(Nat → α → Nat) × α, which turns the hidden environment type into a visible quantified variable. The load-bearing rule is the universe rule for references, Ref A :: Type_{i+1} whenever A :: Type_i, combined with a function typing rule that forces a function's sort to be the same as the sort of its environment. This makes the store inductive over universe levels: a store at one level can only contain closures whose environments live at strictly lower levels, so no reference can appear in the environment of a closure it itself contains. The appendix shows this rule breaks the specific Landin's Knot backpatch by assigning the divergent closure and the reference incompatible sort levels.

What would settle it

Implement the proposed typing rules for simply typed lambda calculus with references and universe levels, then search for any well-typed term that diverges by backpatching; because the proposal leaves function parameters impredicative while restricting only captured environment variables, a natural place to look is a closure that receives the self-referential reference as an argument instead of capturing it. Finding one well-typed diverging term would refute the conjecture; proving normalization would confirm it.

Watch

Extended reading notes

Core claim

The paper's central claim is that higher-order references are not inherently non-terminating; Landin's Knot is well typed only because ordinary function types hide a form of impredicative quantification over the environment. After closure conversion, a closure is an existential pair packaging the code with its environment, and the standard typing of these pairs lets the existentially bound environment type range over the closure's own reference type, which is exactly what makes the cyclic backpatch typecheck. The proposed design makes the environment's sort explicit in the typing rule for functions and adds the rule Γ ⊢ Ref A :: Type_{i+1} whenever Γ ⊢ A :: Type_i, so a reference always points to a type one universe below itself. Under these rules the closure-converted Landin's Knot becomes ill-typed: the closure f needs an environment of sort Type1, while the reference it captures has type Ref(∃α:Type0. ...), and the mismatch blocks the update. The paper states explicitly that termination of the proposed languages has not yet been proven.

Load-bearing premise

The load-bearing premise is that the one-level bump on Ref A rules out every cyclic closure built through the store, not just the single example in the appendix; if a chain of references at increasing levels can still be wired into a backpatch, the conjecture collapses.

Editorial extensions

If this is right

If the conjecture holds, terminating languages can gain higher-order references without adding linear types or giving up the ability to store functions in the store.
The environment sort rule still permits higher-order closures: a closure may capture another closure, as long as the captured closure's type lives at a lower or equal universe level, so the expressiveness loss is aimed precisely at cyclic backpatching.
The proposal makes the store's level structure explicit in the type system rather than in the meta-theory, offering a syntactic alternative to step-indexing for modeling references.
The authors intend to extend the design to dependently typed languages such as the Calculus of Constructions, where it could serve as an intermediate language for a type-preserving compiler with a check-then-link phase.

Reading between the lines

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

A natural next test is to search the proposed calculus for other backpatching encodings, not just the classic one: a level-increasing chain of references that wraps around through an impredicative function parameter would refute the conjecture, so the search should include chains of length two or more.
The Ref rule resembles a syntactic contractiveness condition on store graphs; if made precise, it may imply that every well-typed store is acyclic by construction, which would connect the design to existing work on guarded recursion and step-indexing.
The paper's diagnosis suggests a broader design principle for effects in proof assistants: track the universe level of the environment separately from the types of function arguments, which could simplify adding other effects besides references.
One concrete extension would be to implement the type system for STLC with references and verify that all standard formulations of Landin's Knot fail to typecheck; if any accepted program diverges, the central conjecture is false.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

The paper's real contribution is diagnostic. It reframes Landin's Knot as an impredicativity problem over a function's environment, not as a problem with storing functions in references. That reframing is clear, and the closure-conversion example makes it concrete: the existential that hides the environment type is what lets the reference wrap around its own closure. The paper is also honest that the proposal is a conjecture and that no normalization proof exists. I think the diagnosis will stick, and it is genuinely absent from the cited literature, which tends to model higher-order stores with step-indexing or recursive domain equations rather than ask whether predicative environment sorts could do the job.

The soft spot is exactly where the reader put it: the proposal is a sketch, not a language. There are no typing rules for reference creation or assignment, no store typing, no operational semantics, and no definition of type equality or cumulativity. So the claim that the update in the example is ill-typed rests on an informal argument. The stress-test note worries about cumulativity letting f be coerced to id's type; with standard cumulative universes the coercion goes the wrong direction (Type0 existsentials are subtypes of Type1 existentials, not the reverse), so that particular worry may not land. But the paper never says whether its universes are cumulative, and it never gives the assignment rule, so the type-ill-formedness is not actually verified. More importantly, the general safety claim needs an argument that the level of a store is strictly decreasing along any cycle; the paper gives intuition only.

This is a workshop paper, and it reads like one: a good idea, a worked example, and an open problem. The authors know what they haven't proved. I would not lean on the technical claim yet, but I would cite it as a position and would happily send it to a workshop referee. Anyone working on higher-order store, normalization, or type-preserving compilation should read it. Recommended for a serious referee if the venue welcomes forward-looking conjecture; the referee should ask for a formal definition of the typing and at least a statement of the conjectured normalization theorem.

Engage with it, but as a research prompt rather than a result.

Referee Report

4 major / 5 minor

Summary. The paper argues that Landin's Knot—the encoding of general recursion via backpatching a mutable reference that stores a function—does not follow from higher-order references alone, but from unrestricted (implicitly impredicative) quantification over a function's environment. The authors closure-convert the standard Landin's Knot example, showing that the closure type uses an existential environment type whose universe is unrestricted, and that this is exactly what makes the self-referential update well typed. They then propose two language designs that restrict the environment type: a full-ground restriction and, more promisingly, a universe-level restriction in which the existential quantifier over environments is annotated with a Type_j, and references satisfy Ref A :: Type_{i+1}. With this rule, the closure-converted Landin's Knot example is rejected in Appendix A because id and f receive different universe annotations. The paper does not prove termination; it explicitly states 'We have yet to prove any of these proposed languages terminating' and frames the safety claim as a conjecture.

Significance. If the conjecture is correct, it would offer a significantly simpler route to adding higher-order references to strongly normalizing languages than linear-type approaches, with potential applications to dependently typed intermediate languages. The observation that the impredicativity in function types is what enables Landin's Knot is insightful and is a genuine conceptual contribution, as is the idea of making the store semantics inductive on a universe level. The paper's concrete evidence is thin, however: there is no formal language definition, no operational semantics, no normalization proof, and the only technical demonstration is one derivation showing that a single example becomes ill-typed. The related-work discussion is clear and positions the proposal usefully against step-indexed and recursive-domain models. As a position or vision paper, this is a promising starting point; as a claim of a proven safety property, it is not yet supported.

major comments (4)

[Section 3, 'We have yet to prove...'] The central safety claim—that restricting environment quantification preserves termination—is not established. The manuscript gives no operational semantics, store typing, or normalization argument, and the only concrete evidence is Appendix A's derivation for the single Landin's Knot example. If the intended contribution is a conjecture, the paper should explicitly scope itself as such; if it aims to demonstrate a safety property, a proof (or at least a precise theorem statement and a proof sketch for a defined language) is required.
[Section 3, universe rules and Appendix A] The proposed type system does not specify whether types with different universe annotations are considered equal or whether subsumption/cumulativity is available. In Appendix A, the update r := f is rejected only because id has type ∃α:Type0... and f has type ∃α:Type1... . Under the standard interpretation of Type_i as cumulative with subsumption, f could likely be coerced to the type of id, making the update well typed again and undermining the claimed safety. If the design intentionally rejects subsumption, this must be stated and the consequences for the source language, including whether the original Landin's Knot example is even well typed before the update, must be analyzed.
[Section 3, 'Interpreting the store inductively'] The general claim that the Ref A :: Type_{i+1} rule rules out all cyclic store structures is supported only by intuition and a single example. A chain of references could in principle attempt to form a cycle across multiple reference cells, and the store interpretation is only described informally. The paper needs a formal definition of stores and a proof that the universe-level discipline prevents any cyclic dependency, or at least a precise statement of the invariant and a proof sketch for one concrete language.
[Section 3, language definition] The proposal is under-specified as a language. There is no syntax, no typing judgments for contexts, no evaluation rules, and the source-language rule is informal, using '···' and 'max(...)'. The reader cannot determine which terms are well typed or how the store evolves. A precise definition of at least one of the proposed languages is needed to make the conjecture falsifiable and to assess whether the Ref rule indeed prevents the problematic backpatching.

minor comments (5)

[Section 1] The text contains a typo: 'theupdate to thefunction's environment' should be 'the update to the function's environment'.
[Section 3] The notation for closure types is inconsistent: sometimes the existential is written as ∃α.⟨...⟩ and sometimes as ∃α : Type_j.τ1; choose one notation and use it throughout.
[Section 3] The sentence 'Base types are at level 0' is not accompanied by a formal sort rule for base types; please state explicitly how Nat, functions, and product types receive universe annotations.
[Appendix A] In the derivation D1, the premise Γ,α::Type0 ⊢ (Nat→α→ Nat)×α :: Type0 is shown without making the extended context explicit; include the full context in the derivation to avoid ambiguity.
[Abstract] The phrase 'without restricting references from storing functions' is potentially misleading, since the proposed design does restrict which functions can be stored (only those whose environments are at lower universe levels). Consider rephrasing to 'without forbidding references from storing functions' or 'while still allowing references to store many higher-order functions'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the central claim is an explicit conjecture, and the Appendix derivation is a designed example rather than a derived prediction.

full rationale

The paper does not claim to derive a theorem from first principles; it presents an observation, a conjecture, and a proposed language-design rule. The concrete technical content is the Appendix A derivation showing that, under the proposed sort rules, the closure-converted Landin's Knot example gives `id : ∃α : Type0.(Nat→α→Nat)×α` and `f : ∃α : Type1.(Nat→α→Nat)×α`, so the update `r := f` is ill-typed because the existential annotations differ. This conclusion follows directly from the proposed `Ref A :: Type_{i+1}` rule, which was deliberately designed to produce such a mismatch; that is a design choice, not circular reasoning. There are no fitted parameters renamed as predictions, and no load-bearing self-citation: the only author self-citation, Bowman [4], appears in a future-work sentence about a type-check-then-link compiler and does not justify the conjecture. The paper explicitly labels its main claim a conjecture and admits the lack of a termination proof in Section 3: "We have yet to prove any of these proposed languages terminating." That limitation concerns evidence and completeness, not circularity, so the honest finding is no significant circularity.

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

The paper introduces no fitted numeric parameters. Its central claim rests on three unproven assumptions: that closure-converted existential typing faithfully represents source language functions, that an inductive universe-stratified store semantics is consistent and sufficient for normalization, and that the specific Ref rule prevents all cyclic store configurations. The invented entity is the universe hierarchy for environments and references.

assumptions (3)

domain assumption Closure-converted existential typing (Minamide et al.) is a faithful semantic representation of the source language, so restricting the existential universe of environments restricts source-level closures.
Section 1 introduces closure conversion to expose environments; Section 3 back-translates the closure typing rule to a source function rule without proving equivalence.
domain assumption A store interpreted inductively over universe levels, where each level can only contain functions closing over lower-level stores, is consistent and suffices to guarantee normalization.
Section 3 states this semantics as intuition ("The store at one level will depend only on the interpretation of terms at a lower universe") but does not define or prove it.
ad hoc to paper The universe rule Ref A :: Type_{i+1} is sufficient to prevent all circular dependencies, not just the particular Landin's Knot example.
This is the key new postulate; no proof is provided that no other cyclic store pattern can be typed.

invented entities (1)

Universe-indexed environment sorts and the Ref A :: Type_{i+1} rule
purpose: Force a function's environment to live at a lower universe than any reference containing that function, preventing cyclic closure/store structures.
This new typing construct is introduced solely to rule out Landin's Knot; its consistency and adequacy are not independently established by a normalization proof or implementation.

how reviews work

0 comments

Cite this review

Pith. "Pith review of One Weird Trick to Untie Landin's Knot." pith.science (2026). https://pith.science/paper/IPMITHK7

@misc{pith2026250721317,
  author       = {Pith},
  title        = {Pith review of: One Weird Trick to Untie Landin's Knot},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IPMITHK7}},
  note         = {Machine review of arXiv:2507.21317}
}

read the original abstract

In this work, we explore Landin's Knot, which is understood as a pattern for encoding general recursion, including non-termination, that is possible after adding higher-order references to an otherwise terminating language. We observe that this isn't always true -- higher-order references, by themselves, don't lead to non-termination. The key insight is that Landin's Knot relies not primarily on references storing functions, but on unrestricted quantification over a function's environment. We show this through a closure converted language, in which the function's environment is made explicit and hides the type of the environment through impredicative quantification. Once references are added, this impredicative quantification can be exploited to encode recursion. We conjecture that by restricting the quantification over the environment, higher-order references can be safely added to terminating languages, without resorting to more complex type systems such as linearity, and without restricting references from storing functions.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

11 extracted references · 8 canonical work pages

[1]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundam. Inf. 77, 4 (2007). doi:10.1007/11417170 22

work page doi:10.1007/11417170 2007
[2]

Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State . Ph. D. Dissertation. http://www.ccs.neu.edu/home/ amal/ahmedthesis.pdf

work page 2004
[3]

Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Symposium on Logic in Computer Science (LICS). doi:10.1145/3209108.3209189

arXiv 2018
[4]

William J. Bowman. 2018. Compiling with dependent types . Ph. D. Dissertation. doi:10.17760/d20316239

work page doi:10.17760/d20316239 2018
[5]

A monad for full ground reference cells

Ohad Kammar, Paul B. Levy, Sean K. Moss, and Sam Staton. 2017. A Monad for Full Ground Reference Cells. In Symposium on Logic in Computer Science (LICS) . doi:10.48550/arXiv.1702.04908

work page Pith review arXiv doi:10.48550/arxiv.1702.04908 2017
[6]

Krishnaswami, Pierre Pradic, and Nick Benton

Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Symposium on Principles of Programming Languages (POPL) . doi:10.1145/2676726.2676969

arXiv 2015
[7]

P. J. Landin. 1964. The Mechanical Evaluation of Expressions. Comput. J. (1964). doi:10.1093/comjnl/6.4.308

doi:10.1093/comjnl/6.4.308 1964
[8]

Paul Blain Levy. 2002. Possible World Semantics for General Storage in Call-By-Value. In International Workshop on Computer Science Logic (CSL) . doi:10.1007/3-540-45793-3 16

work page doi:10.1007/3-540-45793-3 2002

Show all 11 references

[9]

Conor McBride. 2016. I Got Plenty o’ Nuttin’. https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf [Online; accessed 24-May-2023]

2016
[10]

Yasuhiko Minamide, Greg Morrisett, and Robert Harper. 1996. Typed closure conversion. In Symposium on Principles of Programming Languages (POPL) . doi:10.1145/237721.237791

1996
[11]

Murawski and Nikos Tzevelekos

Andrzej S. Murawski and Nikos Tzevelekos. 2018. Algorithmic Games for Full Ground References. Formal Methods in Systems Design (2018). doi:10.1007/s10703-017-0292-9 One Weird Trick to Untie Landin’s Knot HOPE’23, September 4–9, 2023, Seattle, Washington, USA A APPENDIX Below w...

2018 doi

Pith tools

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

[1] [1]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundam. Inf. 77, 4 (2007). doi:10.1007/11417170 22

work page doi:10.1007/11417170 2007

[2] [2]

Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State . Ph. D. Dissertation. http://www.ccs.neu.edu/home/ amal/ahmedthesis.pdf

work page 2004

[3] [3]

Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Symposium on Logic in Computer Science (LICS). doi:10.1145/3209108.3209189

arXiv 2018

[4] [4]

William J. Bowman. 2018. Compiling with dependent types . Ph. D. Dissertation. doi:10.17760/d20316239

work page doi:10.17760/d20316239 2018

[5] [5]

A monad for full ground reference cells

Ohad Kammar, Paul B. Levy, Sean K. Moss, and Sam Staton. 2017. A Monad for Full Ground Reference Cells. In Symposium on Logic in Computer Science (LICS) . doi:10.48550/arXiv.1702.04908

work page Pith review arXiv doi:10.48550/arxiv.1702.04908 2017

[6] [6]

Krishnaswami, Pierre Pradic, and Nick Benton

Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Symposium on Principles of Programming Languages (POPL) . doi:10.1145/2676726.2676969

arXiv 2015

[7] [7]

P. J. Landin. 1964. The Mechanical Evaluation of Expressions. Comput. J. (1964). doi:10.1093/comjnl/6.4.308

doi:10.1093/comjnl/6.4.308 1964

[8] [8]

Paul Blain Levy. 2002. Possible World Semantics for General Storage in Call-By-Value. In International Workshop on Computer Science Logic (CSL) . doi:10.1007/3-540-45793-3 16

work page doi:10.1007/3-540-45793-3 2002