This project brings together a diverse set of researchers that maintain practical gradual typing systems including: Reticulated Python, Diamondback Ruby, Typed Racket, Pyret, Typed Clojure, and an emerging gradual type system for the R language. The intention is to identify principles of gradual typing that hold across the spectrum.
Significant open questions:
- Full language integration: None of the existing systems cope with all the features that are found in modern programming languages (e.g. reflection, dynamic code generation).
- Efficient soundness: Researchers have chosen different points in the space between soundness (the type system makes meaningful guarantees ahead of time) and performance (integrations of typed and untyped components may misinterpret bits and behave like C/C++). These decisions have been made on an ad-hoc basis and call for a thorough investigation.
- Empirical evaluation: The design of gradually typed languages must be informed by summative evaluations of gradual typing's feasibility and usefulness. The former calls for studies of every single path from untyped to a typed system; the latter calls for user studies concerning productivity benefits.)
Gradual Typing Across the Spectrum
Gradual Typing Across the Spectrum is funded by the National Science Foundation (SHF 1518844).