Last week, Northeastern hosted a PI meeting for the Gradual Typing Across the Spectrum NSF grant. The meeting was made of 20+ researchers from four institutions, and 12 technical talks. Schedule:

http://prl.ccs.neu.edu/gtp/pi2017/pi2017.html

A common thread among the talks was the question: how to convert a research idea into a tool for software developers?

In my mind, gradual typing is an answer to one instance of this question. The research idea is strong static type systems, and the software developers are the millions using dynamically typed languages. I know that static typing can make programs easier to write and maintain. The developers know that dynamic typing has benefits; moreover they know better than to migrate their code from one language to another on a whim. Gradual typing is a linguistic solution to the problem of adding the benefits of static typing to a dynamically typed language.

Enough opinions, let’s talk about the talks.

The morning session consisted of four talks:

• Milod Kazerounian (UMD) spoke about upgrading the RDL type checker for Ruby with support for refinement types. The idea is to compile Ruby code and types to Rosette, and profit from SMT-assisted type checking.

• Ambrose Bonnaire-Sergeant (IU, slides) has been inferring useful Typed Clojure types through dynamic analysis of Clojure programs. His tool observes how values flow through a program at run-time, then lifts these observations into possibly-recursive, possibly-incorrect type annotations. The surprising result is that the tool quickly (1–2 seconds per unit test, I think) infers types that can help a developer start annotating a program.

• Ben Greenman (NEU, slides) explained why he is implementing a semantics for Typed Racket inspired by Michael Vitousek’s work on Reticulated Python. The “why” is “performance”. The Reticulated semantics will enforce a notion of tag soundness in kind of devils contract to improve performance.

• Preston Tunnell-Wilson (Brown, ONWARD 2017) recently sent questions about programming language design to Mechanical Turk workers. Survey says, developers have extremely diverse opinions about what they expect and what they want regarding scope, inheritance, and infix operators.

In the early afternoon, we had two talks on similar themes as the morning session:

• Andre Kuhlenschmidt (IU) is exploring the design space of efficient implementations for run-time type checks. The main challenge is how to monitor higher-order data in a way that efficiently performs type checks and can help the programmer debug any failed checks. This talk presented data comparing two approaches to the program; I believe the latter, improved approach is based on coercions.

• Zeina Migeed (NEU) explained that there are many ways to adapt type soundness to a gradually typed language, and presented some data comparing Typed Racket’s generalized soudness to Reticulated Python’s tag soundness. The data suggests that tag soundness never adds an order-of-magnitude slowdown.

Next on the schedule were two talks about implementing advanced type systems in Racket’s macro expander (think: meta-level linguistic re-use, capture-avoiding substitution for free!)

• Milo Turner (NEU) first showed how to implement linear and affine type systems using syntax-parse, and second presented a simpler implementation using the Turnstile library.

• David Christiansen (IU) is building a proof assistant in Racket. This talk focused on the design and implementation of proof tactics.

After a short break, we heard about something completely different:

• Justin Pombrio (Brown, ICFP 2017) taught us to interpet the scoping rules of a “core” language as a preorder. Using the preorder, he then showed how to infer the scoping rules of any “surface” language based on its translation to the “core”.

Last summer and fall, Jeremy Siek hosted two REUs (research experience for undergraduates) at Indiana University. The two students gave the next talks:

• Di Zhong (IU) talked about implementing interpreters in Racket, Python, and Haskell. As I understand, this was a hands-on experience through TAPL and the Redex book.

• Zeina Migeed (IU) demonstrated her implementation of conditional types for Reticulated.

Finally,

• Niki Vazou (UMD) presented a theory of gradual refinement types. Any “holes” in the refinements introduce a search problem; type checking attempts to solve the problem by finding a predicate that unifies a function definition and its callers.

This meeting was a great opportunity to reflect on the recent past and share opinions on what’s worth pursuing in the future. Many thanks to the participants, and to the NSF for the support!

If you want to know about the future, you need to ask the young people who will create it. Young people don’t know what can’t be done, and so they go ahead and do it. — Ivan Sutherland