One Weird Trick to Untie Landin's Knot
summary
Claim: Landin’s Knot arises from impredicative quantification over a function’s closure environment, not merely from storing functions in refs. Method: perform closure conversion and expose existential-typed environments, then restrict references’ kinding to create predicative references and a stratified store. Result: impredicativity permits a well-typed self-instantiated environment update; adding predicative refs blocks that update so the cyclic store is ill-typed. Progress: termination is conjectured and approached by induction on store levels plus defunctionalization of closed-function stores; full proof remains work in progress.
AI-written summary · about
chapters (9)
- 0:00Welcome
- 1:05Higher-order references break termination
- 3:52Closures for function environments
- 8:50Predicativity to rule out Landin’s knot
- 11:15Restricting mutable self-reference
- 16:34Stratified store model
- 19:21Termination via defunctionalization
- 21:28Summary and future work
- 22:35Q&A
related talks
12mOn the power of syntactic methods: It is all syntax after all…
14mA Limited Case for Reification by Type Inference
18mDeveloping a Dependently Typed Language with Runtime Proof Search
30mPlausible sealing for gradual parametricity
26mSemantic Encapsulation using Linking Types
15mSealing Pointer-Based Optimizations Behind Pure Functions
25mLocally Nameless Sets
31mDependent tagless final