Deep and Shallow Types for Gradual Languages
summary
Combines deep (natural) and shallow (transient) gradual typing into one language and proves they interoperate while preserving deep’s type soundness and complete monitoring and shallow’s type soundness; deep values cross boundaries via wrappers/proxies while shallow values use lightweight shape checks plus pervasive runtime checks; models and a Typed Racket prototype evaluate 21 GTP benchmarks exhaustively over a 3^n configuration space, finding a high fraction where mixed deep/shallow wins and cutting worst‑case overheads (e.g., from ~4x down to ~2x) except one outlier, zombie.
AI-written summary · about
chapters (5)
- 0:00Start
- 2:00Starting point
- 3:22Key Technical Question
- 9:15Implementation
- 14:12A New Dimension for Cradual Typing
related talks
14mSeeking Stability by being Lazy and Shallow: Lazy and shallow instantiation
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
26mType Narrowing the Hard Way
16mGradually Typing Strategies
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
40mGradualizer: challenges implementing a type checker
13mType Stability in Julia: Avoiding Performance Pathologies in JIT Compilation