Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Tue 22 Oct 2019 10:00 - 10:30 at Abbey - Opening keynote

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.

This program is tentative and subject to change.

Tue 22 Oct

live
09:00 - 10:30: LIVE 2019 - Opening keynote at Abbey
live09:00 - 10:00
Talk
live10:00 - 10:30
Talk