Many mainstream programming languages are dynamically typed. This allows for rapid software development and programming flexibility because it gives programmers the freedom to use powerful programming patterns that are not allowed in statically typed programming languages. Nevertheless, this freedom does not come without drawbacks: static bugs detection, IDE support, and compiler optimization techniques are harder to implement. In the last decades, the research literature and mainstream programming languages have been aiming to reach a trade-off between statically typed and dynamically typed languages. We investigate the trade-off, focusing on the area of optional typing, which allows programmers to choose when to use static type checking in parts of pro- grams. Our primary focus is Dart, an optionally typed programming language with a type system that is unsound by design. What makes Dart interesting from a research point of view is that the static type system combines optional typing with nominal typing using subtyping rules that make the type system unsound even for fully annotated programs. This dissertation contains three main contributions. We first show a for- mal model in Coq of a subset of the Dart type system and operational se- mantics. We prove in Coq that natural restrictions of the Dart type system guarantee the absence of runtime type errors caused by calls to missing meth- ods and functions, without going all the way to full soundness. Our second main contribution concerns the design of a type safety analysis for the full Dart language, and experimental evaluations showing that the algorithm can be successfully applied to real-world programs. Our third main contribution consists of experimentally evaluating the benefits provided by each source of unsoundness in the Dart type system.
Original language
English
Publisher
Department of Computer Science, University of Aarhus
Number of pages
166
Publication status
Published - 2016
Research areas
Dart, Gradual Typing, Optional Typing, Type Systems, Type Inference, Types, Unsound