Applied type-directed semantics

Abstract

Programming language mechanisms with a type-directed semantics are nowadays common and widely used. Such mechanisms include gradual typing, type classes, implicits and intersection types with a merge operator. In these mechanisms with a type-directed semantics, types can alter the result of programs independently. We mainly focus on gradual typing and the merge operator with intersection types. A variant of small-step operational semantics called type-directed operational semantics (TDOS) is recently proposed in a calculus with merge operator and intersection types. Our first goal is to broaden the scope of TDOS. 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. We give the semantics of gradually typed languages directly via the TDOS. Then we study a TDOS with common features. One combination includes the polymorphism, gradual typing and mutable references. Another combination includes polymorphism, merge operator based on intersection types and mutable references. Our second goal is to design applied gradual languages. Mainstream gradually typed languages, such as TypeScript, have OOP features like first-class traits/classes and dynamic inheritance. While there is much theoretical research on gradual typing, most of that research has been focused on gradualizing common calculi. In this work we tend to obtain a foundation for modelling gradually typed languages with both first-class classes and dynamic inheritance. Moreover, because of the spread use of probabilistic programming languages (PPL) in various areas, we aim to bring over the benefits of gradual typing to PPL.