Christos Dimoulas, and
The literature presents many strategies
for enforcing the integrity of types when typed code interacts with untyped code.
This paper presents a uniform evaluation framework that characterizes the
differences among some major existing semantics for typed--untyped interaction.
Type system designers can use this framework to analyze the guarantees of their own dynamic semantics.
Ben Greenman, and
The Brown Benchmark for Table Types (B2T2) provides a focus for research on
type systems for tabular programming via five components:
(1) a definition of tables;
(2) a set of example datasets;
(3) an API of tabular operations with detailed type constraints;
(4) a set of short programs that use the table operations, each of which raises specific typing questions; and
(5) a set of buggy programs with explanations that describe the exact bug in the program.
Christos Dimoulas, and
This paper reports on the surprising difficulties of adapting the Transient
semantics of Reticulated Python to the rich migratory type system of Typed
Racket. The resulting implementation, Shallow Typed Racket, is faster than the
standard Deep Typed Racket but only when the Transient blame assignment strategy is disabled.
For language designers, this report provides valuable hints on how to equip an existing
compiler to support a Transient semantics.
For theoreticians, the negative experience with Transient blame calls for
a thorough investigation of this strategy.
[NEU DRS pdf]
Presents four contributions:
(1) a systematic method to evaluate the performance of a mixed-typed language;
(2) formal properties that measure the strength of types;
(3) a scaled-up Transient semantics; and
(4) the design and implementation of a language that combines Deep types (complete monitoring), Shallow types (type soundness), and untyped code.
The combination helps avoid many worst-of-both-worlds situations
that arise with Deep types only or Shallow types only.
Matthias Felleisen, and
Adapts complete monitoring into a (syntactic, operational) proof
technique for migratory typing.
A semantics satisfies complete monitoring iff it protects all channels
of communication between typed and untyped code.
Introduces blame soundness and blame completeness to
test whether systems that fail complete monitoring can identify
exactly the codes responsible for a run-time type mismatch.
Ben Greenman and
Compares the theory, performance, and implications (for a programmer)
of three approaches to adding types to a dynamically-typed language.
Update 2019-11-13: as it turns out, the paper describes a complete spectrum in ye olde "data processing" sense
(Kelly-Bootle, Stan. The Devil's DP Dictionary. McGraw-Hill Inc. 1981).
spectrum n. plural spectrums; mandatory DP usage wide spectrum(s). [Latin spectrum "an apparition."]
Any range of one or two items or features.
† A range of from three to seven features (the legal maximum) is known as a complete or total spectrum.
Ranges of eight or more are called unfair trading.
Miscellaneous lecture notes here.