A type-safe structure editor calculus
Christian Schmidt Godiksen, Thomas Herrmann, Hans Hüttel, Mikkel Korup Lauridsen, Iman Owliaie · 2020
Structure editors make syntax errors impossible, but they still allow construction of programs with incomplete semantics, leading to program states that cannot be evaluated. We introduce a structure editor calculus for a simple functional programming language that allows for incomplete programs. Our editor expressions may interleave construction and evaluation of programs and can thus describe the history of the development of a program. We extend our editor calculus with types and define a resource-aware type system that prohibits editor expressions introducing type errors in the abstract syntax tree and prove that the type system is sound.