Gradual Soundness: Lessons from Static Python (Programming 7.1)

Kuang-Chen Lu, Ben Greenman, Carl Meyer, Dino Viehland, Aniket Panse, and Shriram Krishnamurthi
[pdf] [bibtex] [artifact] [src] [blog post] [SH]

Static Python is a sound gradual type system for Python by Instagram that can quickly decide whether to allow an untyped value into typed code. How did they do it? With a limited type system that mixes concrete and transient types to allow a tradeoff between strong type guarantees and easy gradual migrations.

Deep and Shallow Types for Gradual Languages (PLDI 2022)

Ben Greenman
[pdf] [supplement] [slides] [bibtex] [src] [SH]

Deep gradual types offer compositional guarantees but depend on expensive higher-order contracts. Shallow types enforce only local properties, but can be implemented with first-order checks. This paper presents a language design that supports both deep and shallow types to utilize their complementary strengths. Coming soon to Typed Racket:

Types for Tables: A Language Design Benchmark (Programming 6.2)

Kuang-Chen Lu, Ben Greenman, and Shriram Krishnamurthi
[pdf] [supplement] [bibtex] [src]

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.

A Transient Semantics for Typed Racket (Programming 6.2)

Ben Greenman, Lukas Lazarek, Christos Dimoulas, and Matthias Felleisen
[pdf] [bibtex] [slides] [youtube] [private src]

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.

How to Evaluate Blame for Gradual Types (ICFP '21)

Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas
[pdf] [bibtex] [youtube]

Is blame information helpful? We generated programs with type boundary errors and simulated a rationally-acting programmer to find out. The results confirm the theory, but only barely.

Deep and Shallow Types (Ph.D. dissertation, December '20)

Ben Greenman
[pdf] [bibtex] [slides] [youtube] [src] [NEU DRS pdf] [ProQuest]

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.

Complete Monitors for Gradual Types (OOPSLA '19)

Ben Greenman, Matthias Felleisen, and Christos Dimoulas
[pdf] [supplement] [bibtex] [slides] [youtube] [src]

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.

How to Evaluate the Performance of Gradual Type Systems (JFP '19)

Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen
[pdf] [bibtex] [slides] [video abstract] [mp4 source]

Archival version of Is Sound Gradual Typing Dead?. Evaluates the relative performance of different gradual typing systems for the same language, and introduces a method based on simple random sampling to approximate the number of D-deliverable configurations in a program.

Note: The data for the zordoz benchmark is flawed; in fact, there is little improvement between v6.2 and v6.4 on this benchmark. For details, see the release notes for version 3 of the GTP benchmark suite.

The Behavior of Gradual Types: A User Study (DLS '18)

Preston Tunnell Wilson, Ben Greenman, Justin Pombrio and Shriram Krishnamurthi
[pdf] [bibtex] [slides] [data]

Presents the results of surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics.

Collapsible Contracts: Fixing a Pathology of Gradual Typing (OOPSLA '18)

Daniel Feltey, Ben Greenman, Christophe Scholliers, Robert Bruce Findler, and Vincent St-Amour
[pdf] [bibtex]

Design and evaluation of ``space-efficient'' contracts for Racket. Really the contracts are time and space efficient because they are collapsible (i.e. support a merge operation). The implementation is based on Michael Greenberg's model of eidetic contracts.

A Spectrum of Type Soundness and Performance (ICFP '18)

Ben Greenman and Matthias Felleisen
[pdf] [supplement] [bibtex] [slides] [youtube] [src] [redex models] [artifact]

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.

On the Cost of Type-Tag Soundness (PEPM '18)

Ben Greenman and Zeina Migeed
[pdf] [bibtex] [slides] [script] [poster] [artifact]

Systematically evaluates the performance of Reticulated. Introduces a method for approximating the number of D-deliverable configurations in a benchmark through simple random sampling. Validates the method with: (1) a tiny bit of statistics, and (2) by comparing some approximations to the ground truth.

Migratory Typing: 10 Years Later (SNAPL '17)

Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, Asumu Takikawa
[pdf] [bibtex]

Reflections on Typed Racket.

Type Systems as Macros (POPL '17)

Stephen Chang, Alex Knauth, Ben Greenman.
[pdf] [bibtex] [artifact]

Type systems enforce a syntactic discipline on programmers (language users). Macros systems let programmers (language designers) change the syntax of their language. This paper argues that a macro system is an ideal vehicle for implementing type systems.

Is Sound Gradual Typing Dead? (POPL '16)

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen.
[pdf] [bibtex] [poster] [artifact]

Proposes a method for evaluating the performance of gradual type systems.

Position Paper: Performance Evaluation for Gradual Type Systems (STOP '15)

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen.
[pdf] [bibtex] [slides]

Gradual type systems need comprehensive performance evaluation, and this evaluation needs to benchmark all ways of gradually typing example programs. Just checking the fully-untyped and fully-typed versions of a program is not enough!

Getting F-Bounded Polymorphism into Shape (PLDI '14)

Ben Greenman, Fabian Muehlboeck, Ross Tate (and wisdom from the Ceylon team).
[pdf] [bibtex] [poster] [teaser] [slides]

We show how to achieve decidable subtyping in object-oriented languages and argue that our approach is backwards compatible with existing Java projects.

Miscellaneous lecture notes here.