Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Well-Typed Programs Can’t Be Blamed
verfasst von : Philip Wadler, Robert Bruce Findler
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We introduce the
blame calculus
, which adds the notion of blame from Findler and Felleisen’s
contracts
to a system similar to Siek and Taha’s
gradual types
and Flanagan’s
hybrid types
. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtypes, and show that these recombine to yield naive subtypes. Naive subtypes previously appeared in type systems that are unsound, but we believe this is the first time naive subtypes play a role in establishing type soundness.