Gradual typing is morally incorrect; we're all monsters now

Abstract

The aspiration of gradual typing — that typed and untyped code can coexist happily, with errors reported at runtime when the types are found to be wrong — has led many languages, including our own, to adopt the paradigm. The practice is different; even the term itself has been refined short of this aspiration, and languages abdicate their responsibilities as soon as they become too onerous: when an object reënters dynamically-typed code, in the presence of aliasing, or with regard to secure object identity.

A type assertion should be meaningful. Aliases of the same object ascribed different types, the collapse of variant or generic types, objects passed to dynamically-typed code with the understanding that they had a particular type, and even past behaviour, are all routes through which an assertion can be falsified, but all practical gradual systems ignore some or all of these cases. The level of knowledge the system has can change behaviour, and the only morally correct behaviour is to retain an impossibly complete level of information on the types of objects.

Authors

Timothy Jones, Michael Homer

Published in

Workshop on New Object-Oriented Languages (NOOL), 2015

Resources

Author copy (PDF)
Presentation slides (PDF)

PDF: mwh.nz/pdf/nool2015
this page: mwh.nz/pubs/nool2015