Iterative Typing

Abstract

Types have been introduced into programming languages to increase safety and the abstraction level ; with typing, programmers do no longer directly manipulate byte strings but data of a certain type instead. Type systems must make a compromise between static safety and expressiveness ; static safety being the ability to detect errors based on a static code analysis and expressiveness being the ability to denote concepts. Traditionally, programming languages are separated into two classes: statically typed languages and dynamically typed languages. The first class emphasises early error detection and catches many errors during static code analysis. The second emphasises expressiveness but catches errors very lately, right before calls to built in functions. The gap between those two classes is considerable and we argue that the best of those two worlds can be combined. The compromise this thesis defends is called iterative typing. In essence, iterative typing is a static typing that delays as little checks as possible for runtime. When an uncertainty occurs during static code analysis, static typings typically make assumptions that allows to continue the analysis but inhibit the expressiveness of the language. In the same situation, iterative typing inserts annotations into the code so the uncertainty can be precisely resolved at runtime, when more information will be available. Iterative typing shines when type deduction depends on the executed branch of a conditional structure like it is the case for dispatch on types and deserialization patterns. As a validation of iterative typing we present three case studies of practical interest ; although the exposed solutions are implemented in a dynamic way, iterative typing is able to catch errors early on.

Date of Award	15 Sep 2013
Original language	English
Supervisor	Wolfgang De Meuter (Promotor)