Gradual typing is a principled approach to integrating static and dynamic type checking. To clarify what gradual typing means, Siek and collaborators articulated criteria for gradually typed languages: essentially that type checking and execution must smoothly transition between the two type checking regimes. However, these criteria say nothing about the relationship between the semantics of gradual and static types. This absence, which can be ascribed to gradual typing’s tendency to focus on simple types, becomes critical for advanced type disciplines, where type \emph{safety} does not imply type \emph{soundness}.

We assert a semantic criterion for gradual types. To coherently blend static and dynamic checking of a particular type discipline, a gradual type system must enforce the same invariants as those \emph{intended} by its purely-static counterpart. We justify this stance by considering several type disciplines, highlighting key challenges and opportunities.