Staged Gradual Typing

Staging dynamically typed programming languages safely is a challenge, as the programming-language support for staged computation typically relies on static type systems. To solve this problem, we propose a staged gradual type system that seamlessly integrates static and dynamic typing with staged computation. Our system combines the basic gradual type system and the let-polymorphic staged type system for run-time code generation safely. We discuss the design and issues in developing the calculus, and present a type system and operational semantics via a translation to a cast calculus where dynamic type checking is made explicit. We also show several applications, such as lightweight stage polymorphism.