Type-directed operational semantics for gradual typing

Abstract

The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In a TDOS, type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, type annotations are used to trigger type-based conversions on values. We illustrate how to employ a TDOS on gradually typed languages using two calculi. The first calculus, called λB^g, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λe, explores an eager semantics for gradually typed languages using a TDOS. For both calculi, type safety is proved. For the λB^g calculus, we also present a variant with blame labels and illustrate how the TDOS can also deal with such an important feature of gradually typed languages. We also show that the semantics of λB^g with blame labels is sound and complete with respect to the semantics of the blame calculus, and that both calculi come with a gradual guarantee. All the results have been formalized in the Coq theorem prover.