Gradual typing is morally incorrect; we're all monsters now
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 reë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.
Timothy Jones, Michael Homer
Workshop on New Object-Oriented Languages (NOOL
Michael Homer — 2018