Type unsoundness in practice: An empirical study of dart

Gianluca Mezzetti, Anders Møller, Fabio Strocco

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

224 Downloads (Pure)

Abstract

The type system in the Dart programming language is deliberately designed to be unsound: for a number of reasons, it may happen that a program encounters type errors at runtime although the static type checker reports no warnings. According to the language designers, this ensures a pragmatic balance between the ability to catch bugs statically and allowing a flexible programming style without burdening the programmer with a lot of spurious type warnings. In this work, we attempt to experimentally validate these design choices. Through an empirical evaluation based on open source programs written in Dart totaling 2:4 M LOC, we explore how alternative, more sound choices affect the type warnings being produced. Our results show that some, but not all, sources of unsoundness can be justified. In particular, we find that unsoundness caused by bivariant function subtyping and method overriding does not seem to help programmers. Such information may be useful when designing future versions of the language or entirely new languages.

Original languageEnglish
Title of host publicationDLS 2016 - Proceedings of the 12th Symposium on Dynamic Languages
EditorsRoberto Ierusalimschy
Number of pages12
PublisherAssociation for Computing Machinery
Publication date1 Nov 2016
Pages13-24
ISBN (Print)978-1-4503-4445-6
ISBN (Electronic)9781450344456
DOIs
Publication statusPublished - 1 Nov 2016
EventSPLASH 2016: Systems, Programming, and Applications - Amsterdam, Netherlands
Duration: 30 Oct 20164 Nov 2016
http://2016.splashcon.org/

Conference

ConferenceSPLASH 2016
Country/TerritoryNetherlands
CityAmsterdam
Period30/10/201604/11/2016
Internet address

Keywords

  • Gradual typing
  • Language design
  • Type systems

Fingerprint

Dive into the research topics of 'Type unsoundness in practice: An empirical study of dart'. Together they form a unique fingerprint.

Cite this