Reproduce “One Weird Trick to Untie Landin's Knot” on OpenResearch

About this paper

Paulette Koronkevich, William J. Bowman

Researchers at the University of British Columbia introduce a re-interpretation of Landin's Knot, asserting that its cause is unrestricted quantification over function environments, not merely storing functions. Their proposed language design employs explicit universe levels for environments and references, which effectively prevents divergent circular dependencies and aims to preserve strong normalization in functional languages.

Key insights

• Landin's Knot is not solely due to functions being stored in references, but rather stems from the unrestricted, impredicative quantification over the type of a function's environment, enabling circular dependencies.
• Closure conversion effectively uncovers this implicit impredicativity, revealing how self-referential cycles leading to non-termination become well-typed under standard rules.
• Introducing predicative universe levels to explicitly constrain the types of function environments and references can systematically break the problematic circularity that causes Landin's Knot.

Summary by alphaXiv.