As part of the grand goal of bringing live programming and “real programming” together, static types pose a UX challenge: How to bring the benefits of static checking without ruining the “liveness” of a system? How to make a live programming environment which is also intended for serious programming?
“Steady Typing” is our approach to reconcile static types with live programming.
Before describing the approach, I intend to motivate it by opening the talk with a brief overview of my personal journey from dynamic languages (BASIC) to static ones (C/C++), back to dynamic (Python) and back again to static (Haskell) - which also serves as a reflection of industry trends. During this introduction I’ll briefly illustrate trade-offs between approaches to types, and also how type inference affects the trade-offs while introducing new pain points.
I’ll then describe and demonstrate the Steady Typing approach, which consists of three mechanisms:
- The edited programs always type-check. “Fragments” (aka “non empty holes”) are introduced around edits which would had otherwise resulted in type errors (previously demonstrated in FPW 2014, LIVE 2018)
- An “insist type” feature lets the user reassign the blame for type mismatches, by defragmenting a selected fragment and introducing fragments around other sources of conflict instead.
- To avoid refragmentations crossing global definition boundaries, type mismatches across global definitions are handled by “freezing” the dependency types for each definitions, and using those when inferring the type for this definition. Dependencies whose types have changed present a call to action which propagates the dependency type update into the current definition and introducing fragments in it if necessary.