Managing Gradual Typing with Message-Safety in Dart

Publikation: KonferencebidragPaper



This paper establishes a notion of message-safe programs as a natural intermediate point between dynamically typed and statically typed Dart programs.
Unlike traditional static type checking, the type system in the Dart programming language is unsound by design. The rationale has been that this allows compile-time detection of likely errors and enables code completion in integrated development environments, without being restrictive on programmers. We show that, despite unsoundness, judicious use of type annotations can ensure useful properties of the runtime behavior of Dart programs. This supports evolution from a dynamically typed programto a strictly statically typed form.
We present a formal model of Dart that elucidates how a core of the language and its standard type system works. This allows us to characterize message-safe programs and present a theorem stating that such programs will never cause ‘message not understood’ errors, which is generally not guaranteed for Dart programs that pass the standard type checker. The formal model has been expressed in Coq.
Antal sider15
StatusUdgivet - 2014
BegivenhedInternational Workshop on Foundations of Object-Oriented Languages - Portland, USA
Varighed: 20 okt. 201420 okt. 2014
Konferencens nummer: 21


WorkshopInternational Workshop on Foundations of Object-Oriented Languages

Bibliografisk note

An informal proceedings will be made publicly available on this web page. However, presentation at FOOL does not count as prior publication, and many of the results presented at FOOL have later been published at ECOOP, OOPSLA, POPL, and other main conferences.

Se relationer på Aarhus Universitet Citationsformater


Ingen data tilgængelig

ID: 84296326