Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation
summary
Formalizing a type-system family parameterized by eager vs lazy and deep vs shallow instantiation, the work proves stability properties (type-preserving let inlining, duplication of equations, eta-expansion) and produces concrete counterexamples where properties break. Mechanized proofs and counterexamples live in the paper; comparing all four quadrants yields a single recommendation for GHC10: lazy shallow instantiation preserves most of the stability laws though not all, so it minimizes surprising regressions when definitions are eta-expanded, inlined, or duplicated.
AI-written summary · about
chapters (4)
related talks
13mType Stability in Julia: Avoiding Performance Pathologies in JIT Compilation
36mWorking Hard to Keep Things Lazy
46mRefinement Types from Light to Deep Verification
30mDotty and types: the story so far
19mIll-Typed Programs Don't Evaluate
17mApproximating Type Stability in the Julia JIT
25mShallowly embedding type theories
12mOn the power of syntactic methods: It is all syntax after all…