abstract.tex

\begin{abstract}
Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. 
This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. 
This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states.
% As a secondary contribution, we show how total marking resolves 
% the problem of undefined behavior in the Hazelnut structure editor calculus
% (though marking itself does not require a structure editor).

The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. 
Constraint-based type inference can bring more distant information to bear in discovering
inconsistencies but this notoriously complicates error localization. We approach this problem by
deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed
core. Errors arising from inconsistent unification constraints are localized exclusively to type and
expression holes, i.e., the system identifies unfillable holes using a system of traced  provenances, rather than localized in an \emph{ad hoc} manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel. 
\end{abstract}

% Lacking formal foundations, error localization has largely become a matter of folklore in the community. 
% Recent work on the Hazelnut calculus takes a step toward assigning formal meaning to erroneous programs, but it stops short of a comprehensive account. 
% In particular,  (1) Hazelnut is able to reason around marked type inconsistencies, but not several other kinds of static errors, and (2) Hazelnut provides an insufficient account of the marking procedure itself, relying on a limited structure editor, or on the user, to correctly insert marks.\todo{decenter Hazelnut?}