One Weird Trick to Untie Landin's Knot
Paulette Koronkevich, William J. Bowman

TL;DR
This paper investigates how Landin's Knot, a pattern for encoding recursion, can be exploited using higher-order references and impredicative quantification, revealing conditions under which non-termination can be encoded.
Contribution
It identifies that Landin's Knot relies on environment quantification and shows how impredicative quantification enables recursion with references, suggesting restrictions could prevent non-termination.
Findings
Higher-order references alone do not cause non-termination.
Impredicative quantification over environments enables encoding recursion.
Restricting environment quantification may prevent non-termination in typed languages.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
