ABSTRACT. Gradually typed languages, including Typed Racket, Typescript, Thorn and Reticulated Python, facilitate interoperability between statically and dynamically typed code, by checking static types when available and applying dynamic type checks when not. However, almost all exisiting research studies gradually typed languages using operational semantics, designed in an ad hoc manner. Furthermore, in the operational setting, questions of program equivalence and other relational properties are difficult to study and for the most part ignored.

In this paper, we propose a type-theoretic and category-theoretic semantics for gradual typing, in the form of gradual type theory, a logic and type theory for (call-by-name) gradual typing. To define the central constructions of gradual typing (the dynamic type, type casts and type error) in a type-theoretic fashion, we extend the theory of types and terms to include gradual type and term precision, internalizing notions of ``more dynamic'' into the type theory and then using these to characterize the constructions of gradual typing uniquely. This includes a novel specification for casts in terms of type and term precision. Combined with the ordinary extensionality ($\eta$) principles that type theory provides, we show that most of the standard operational behavior of casts in a gradually typed language are in fact uniquely determined by our design constraints. This provides a semantic justification for the definitions of casts and also shows that non-standard definitions of casts must violate these principles. We explore a call-by-name type theory in this paper, because it is a simple setting with the necessary extensionality principles, leaving call-by-value to future work.

On the category-theoretic side, we show that our type theory is an internal language of a certain class of double categories called called equipments (in fact, we will use only preorder categories, which are double categories where one direction is posetal), which provides the right algebraic structure with which to interpret precision and casts in gradual typing. We apply this categorical semantics to give a general construction of models of gradual typing, which provides a semantic analogue of Findler and Felleisen's definitions of contracts, and generalizes Dana Scott's domain-theoretic models of dynamic typing.