One Weird Trick to Untie Landin's Knot

Explore Landin's Knot and its relationship to general recursion and non-termination in programming languages. Delve into the insight that higher-order references alone don't necessarily lead to non-termination, but rather the unrestricted quantification over a function's environment is the key factor. Examine a closure converted language that makes the function's environment explicit and uses impredicative quantification to hide the environment's type. Investigate how this impredicative quantification can be exploited to encode recursion when references are added. Consider the possibility of safely adding higher-order references to terminating languages by restricting quantification over the environment, without resorting to complex type systems or limiting references from storing functions.

[HOPE'23] One Weird Trick to Untie Landin's Knot