1 Introduction↩︎

Programming often involves reasoning about static types. Development tools assist programmers in limited ways with this task, e.g. by reporting the type of an expression when hovering over it, or reporting the expected and actual type when there is a type error. However, these services only report what the type of an expression is, not why it is that type in the context of the surrounding program. Programmers must hunt through the program themselves to answer these questions, and the program often contains a large volume of code irrelevant to their query.

This paper develops the theory of type slicing from type-theoretic first principles. Type slices allow developers to ask “why questions” [1] about type information reported about arbitrary terms within a (possibly incomplete or erroneous) program. The answers are given in the form of a minimal slice of the original program (i.e. a program with unrelated terms folded away) that suffices to reproduce the queried type. Type slicing is inspired in principle by prior work on program slicing (§[sec:related-work]), in particular, lattice-based Galois slicing [2]–[6]. However, slicing is here applied to a (non-Galois) static type checking setting, loosely more akin to type-error slicing [7]–[9], and the concurrent independently researched work on type-directed slicing [10] for Java.

We consider the problem of type slicing in the context of bidirectional type systems [11], which distinguish type synthesis (which type does this term have) from type analysis (which type is expected). Correspondingly, a synthesis slice (§4) of a selected term answers “which parts of the program caused it to have type \(\tau\)?” and an analysis slice (§6) answers the complementary question, “which parts of the surrounding program enforced that this term have type \(\tau\)?” Formalising analysis slices requires a novel context typing construction (§5), which types the one-hole context surrounding a focused sub-term. Queries can be refined, say from an entire function type to just its codomain, resulting in a smaller slice. This allows a programmer to incrementally focus on sub-parts of the type that are of interest, for example, determining that only a small region of a large record type involved in a type error is erroneous.

1.0.0.1 Type Error Debugging

The type slicing machinery applies equally well to well-typed and ill-typed terms. In the case of ill-typed terms, it provides a mechanism that may aid in debugging type errors, subsuming the question of “why is this term a type error?” This is achieved by integrating type slicing with the theory of error marking (§7). A distinguishing feature of type slicing is that a slice is itself a valid incomplete program that preserves the original’s shape; in Hazel [12], which allows incomplete programs, this is simply a valid program. Type slicing therefore composes with most other type debugging methods, as we can simply run them on the minimised programs.

For example, error localisation [13], [14] and counter-factual [15]–[17] type debugging techniques (§11.5) are equally applicable, and in fact simpler, on minimised programs, when their language assumptions (typically global inference) apply.

Further, editing the ‘type’ of an expression as suggested by such tools is not necessarily easy when the surrounding context expects a different type. The analysis slice points to the surrounding terms (typically annotations) that must be modified to make such an edit, likewise easing refactoring to a different type in general.

1.1 Contributions↩︎

The theory applies to bidirectional type systems with any form of downwards static graduality on expressions (§2), inspired by the gradual typing literature [18] extended to incomplete programs, i.e. programs with holes (and marked errors). No cast dynamics are required, so type slicing applies to any bidirectional system upon assigning a precision relation on types and terms (§3.2).

Concretely, this paper contributes: (i) a core calculus with holes, products, sums, and explicit polymorphism, based on the Hazelnut and marked lambda calculi [19], [20], with precision lattices satisfying graduality (§3); (ii) synthesis slices (§4), whose minimal slices exist for every query, refine monotonically, and decompose compositionally; (iii) context typing (§5), a novel judgement with totality, soundness, and gradual guarantees, enabling the dual analysis slices (§6); (iv) integration with error marking (§7), extending both slice forms to arbitrary ill-typed programs; (v) term-minimal slices supporting compositional calculation, NP-hardness of minimum-size slicing, and a linear-time approximation (§8–§10); and (vi) a comparison with prior forms of slicing and type debugging, and applications to set-theoretic and occurrence typing (§[sec:related-work]).

Hazel [12] is an example full-scale language satisfying these conditions; we have extended its implementation with an efficient linear-time approximation of type slicing, introduced by example (§1.2). The prototype user interface is an initial proof of concept, and we make no specific usability claims; we expect the theory to support a variety of user interfaces and further applications for type debugging and explanation, and suggest several avenues for exploration (§12). The core calculus and metatheory are mechanised in Agda and available in the supplemental material.

1.2 Type Slicing in Hazel by Example↩︎

This section previews type slicing, formally developed later (§4, §6) over the core calculus (§3), through two worked examples in the Hazel implementation. The Hazel UI has a cursor inspector at the bottom of the screen which details which type the selected term has, and what it expects; these are the respective types to calculate a synthesis slice and an analysis slice for.

Hazel renders each slice by folding away every fragment the queried type does not require. The user can refine their slice by themselves folding away part of the type being sliced, which will correspondingly fold away additional fragments of the program.

[fig:parse-digit-synthesis] slices a small character parser. The synthesis slice reduces the function to the String domain annotation and the first branch determining the result option type, discarding all other branches.¹

Refined queries may target part of a reported type: for example, asking only about the domain of a function type, by folding away the returned sum type (String ->\({\color{teal}\Box}\)). The resulting program shrinks the slice to exclude the entire function body (2). This same slice is also the minimal analysis slice which enforces String on the argument.

3 considers a much more complex error where a sequencing parser combinator has been defined incorrectly, but used correctly. As is usual, the error has been incorrectly localised to the usage site, trusting the (incorrect) annotation. Specifically, seq’s continuation is annotated as if it returns an Option immediately, rather than first accepting the remaining String threaded out of the previous parser. The use site provides the intended parser continuation.

Explain error queries the slices on only the outermost inconsistency in the types (the function vs the option in the return type); the resulting slice collapses the program to just the function shape of the continuation and the offending annotation.

Crucially, the slice did not assume the annotation is the ground truth. It shows the user both the expectation’s source (the annotation) and the usage (the function), leaving the programmer to judge which is wrong. This is justified as programmers often add annotations incorrectly to existing code (49% of the time [21]).

Should the user instead wish to trust the context unilaterally, they can simply only consider the synthesis slice (omitting the analysis slice entirely). We later make slicing of type errors precise, applying slicing to marked ill-typed programs (§7).

2 Language Scope↩︎

This section introduces the key characteristics of the languages to which type slicing can be applied.

2.1 Bidirectional Types↩︎

Type slicing is formalised for bidirectional type systems [11]. Such a type system is an algorithmic specification of typing judgements, naturally lending itself to direct typing algorithms which do not require guessing of types during type checking. These systems do require annotations, but annotation burden is lessened by locally inferring types [22].

This is achieved by specifying the mode of the type parameter in a typing judgement, distinguishing when it is an input (type analysis/checking) and when it is an output (type synthesis): \[\Delta;\,\Gamma \vdash e \mathrel{{\color{BrickRed}\Rightarrow}}\tau\] Read as: \(e\) synthesises type \(\tau\) under typing assumptions \(\Gamma\) and type variable assumptions \(\Delta\). The type \(\tau\) is an output. \[\Delta;\,\Gamma \vdash e \mathrel{{\color{BlueViolet}\Leftarrow}}\tau\] Read as: \(e\) analyses against type \(\tau\) under typing assumptions \(\Delta, \Gamma\). The type \(\tau\) is an input. This is where the terminology of synthesis / analysis slices is derived from.

Such languages have two fundamental rules: \[\inference[\mathrm{\small SVar}]{x : \tau \in \Gamma}{\Delta;\,\Gamma \vdash x \mathrel{{\color{BrickRed}\Rightarrow}}\tau} \qquad \inference[\mathrm{\small Sub}]{\Delta;\,\Gamma \vdash e \mathrel{{\color{BrickRed}\Rightarrow}}\tau}{\Delta;\,\Gamma \vdash e \mathrel{{\color{BlueViolet}\Leftarrow}}\tau}\] Variables synthesise their type from the typing assumptions. Subsumption bridges the two modes: any term that can synthesise a type also analyses against that same type.

2.2 Downwards Static Graduality↩︎

To calculate a type slice we will need a way to gradually omit sub-expressions from the program, and type check these less ‘precise’ partial programs at less or equally ‘precise’ types. Formally, precision must form two partial orders (notated \(\mathrel{{\color{latticecolor}\sqsubseteq}}\)) over types and expressions, which can be lifted onto typing assumptions \(\Gamma\).

For example, this precision order can correspond to the precision relation on types in a gradually typed system [23]. In this situation this graduality theorem corresponds to the downwards static case² of the graduality theorem in the refined criteria for gradual types [18], adapted to a bidirectional setting. The calculus we demonstrate type slicing on in this paper goes even further by allowing maximally incomplete programs, omitting any program sub-expression, based upon the Hazel calculus [24].

Although not necessary, it is also useful that precision forms a lattice with meets and joins to perform optimisations to type slicing calculation (§8).

3 The Core Calculus↩︎

In this section, we present the core calculus which type slicing builds upon. It is a bidirectional, gradually typed lambda calculus, with precision on types and terms, based on the Hazel calculus [24], extended with products, sums, and explicit System F polymorphism. We prove that this calculus satisfies graduality (§2.2), and we define and prove several lattice structures on precision.

3.1 Syntax & Relations↩︎

The syntax of the core calculus is given in Figure 4. \(1\) is the unit type, and \({\color{teal}\Box}\) is a gap / hole serving a dual role: in the gradual typing interpretation it is the dynamic type, and in the slicing interpretation it represents unrequired type information (to explain a query). Similarly a \({\color{teal}\Box}\) in expressions represents omitted sub-expressions, irrelevant to the explanation resulting from a query. In type checking, omitted expressions synthesise the dynamic (omitted) type.

None

Base types such as booleans are omitted from the core syntax, being encoded using sums in the usual way (e.g.\(\mathit{Bool} \triangleq 1 + 1\)); we use them freely in examples.

3.1.1 Consistency↩︎

Type consistency (Figure 5) is exactly as presented in standard gradual type systems (§2.2). That is, a weakening of equality, where every type is consistent with \({\color{teal}\Box}\), and compound types are consistent when their components are. Consistency is reflexive and symmetric but not transitive.

None

3.1.2 Precision↩︎

Precision (Figure 6) is a partial order that organises terms by information content: for types, \(\tau' \mathrel{{\color{latticecolor}\sqsubseteq}}\tau\) means \(\tau\) has at least as much type information as \(\tau'\). Here, \({\color{teal}\Box}\) is the global minimum. Expression precision is defined analogously; for instance, the slices of \(\lambda x \mathbin{:} 1.\; x\) form the precision chain \({\color{teal}\Box}\mathrel{{\color{latticecolor}\sqsubseteq}}\lambda x \mathbin{:} {\color{teal}\Box}.\; {\color{teal}\Box}\mathrel{{\color{latticecolor}\sqsubseteq}}\lambda x \mathbin{:} 1.\; {\color{teal}\Box}\mathrel{{\color{latticecolor}\sqsubseteq}}\lambda x \mathbin{:} 1.\; x\), each step filling in one more part of the term.

None

3.1.2.1 Precision on Typing Assumptions.

In this calculus, we represent typing assumptions as finite partial functions from variable names to types, with domain \(\mathrm{dom}(\Gamma)\). Precision is defined by domain inclusion and pointwise precision on types in the (smaller) domain: \[\gamma_1 \mathrel{{\color{latticecolor}\sqsubseteq}}\gamma_2 \iff \mathrm{dom}(\gamma_1) \subseteq \mathrm{dom}(\gamma_2) \text{ and } \gamma_1(x) \mathrel{{\color{latticecolor}\sqsubseteq}}\gamma_2(x) \text{ for all } x \in \mathrm{dom}(\gamma_1)\] That is, a less precise type assumptions set either assumes fewer variables’ types, or assumes less precise types on the present variables.

3.2 Lattice Properties↩︎

3.2.1 Meets and Joins↩︎

The meet \(\tau_1 \mathbin{{\color{latticecolor}\sqcap}}\tau_2\) is the greatest lower bound (GLB) under precision, retaining only sub-terms present in both terms. The join \(\tau_1 \mathbin{{\color{latticecolor}\sqcup}}\tau_2\) is the least upper bound (LUB) under precision, omitting only subterms omitted in both components. For example: \[(1 \mathbin{\to}{\color{teal}\Box}) \mathbin{{\color{latticecolor}\sqcap}}({\color{teal}\Box}\mathbin{\to}1) \;=\; {\color{teal}\Box}\mathbin{\to}{\color{teal}\Box}, \qquad\quad (1 \mathbin{\to}{\color{teal}\Box}) \mathbin{{\color{latticecolor}\sqcup}}({\color{teal}\Box}\mathbin{\to}1) \;=\; 1 \mathbin{\to}1.\] Meets are total, but joins are defined only between consistent types.

3.2.2 The Slice Lattice↩︎

For a fixed type \(\tau\), the slice lattice of \(\tau\) is the lower set under precision: \[\lfloor\tau\rfloor \;=\; \{\,\upsilon \mid \upsilon \mathrel{{\color{latticecolor}\sqsubseteq}}\tau\,\}\] \(\lfloor e \rfloor\), \(\lfloor \mathcal{C}\rfloor\), and \(\lfloor \Gamma \rfloor\) are defined analogously for expressions, contexts, and assumptions. Each slice lattice has top \(\top = \tau\) and bottom \(\bot = {\color{teal}\Box}\). Then precision, meets, and joins simply lift unchanged into the slice lattice. Importantly all terms in the slice lattice are consistent, so joins are always defined:

Hence, all terms in the slice lattice are consistent, making it a well-defined bounded lattice. The meet and join are also distributive. Further, slice lattices are trivially finite:

Moreover, being finite and distributive, each slice lattice is bi-Heyting [26]. We will later introduce and use co-Heyting subtraction to represent ‘disjoint’ types (§8).

3.2.2.1 Notation: Slice Lattices as Highlighted Terms.

An element of a slice lattice can be notated as a highlight of the original (top) term with omitted regions (the \({\color{teal}\Box}\)s) left unhighlighted. For instance, the slice \(\mathit{Int} \mathbin{\to}{\color{teal}\Box}\) in \(\lfloor\mathit{Int} \mathbin{\to}\mathit{Bool}\rfloor\) can be represented as \(\def\sli@c{NavyBlue} \def\sli@style{dashed} \ifx\sli@c OliveGreen\def\sli@style{dotted}\fi \ifx\sli@c teal\def\sli@style{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=NavyBlue!60, \sli@style, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=NavyBlue!12, anchor=base] (N) {\strut\mathit{Int} \mathbin{\to}}; } \, \mathit{Bool}\).

3.3 Typing Rules↩︎

The bidirectional typing judgements are mostly standard; the complete synthesis and analysis rule sets appear in the supplementary material, and Figure 7 presents some of the major rules. \(\Delta \vdash \tau\;\mathsf{wf}\) denotes when a type \(\tau\) is well-formed under available type variables \(\Delta\).

None

We use joins to replicate type matching in the gradual typing literature.³ \(\tau \equiv \tau_1 \mathbin{\to}\tau_2\) extracts the domain and codomain of \(\tau\), or the gap type \({\color{teal}\Box}\) if \(\tau \equiv {\color{teal}\Box}\). Case expressions can synthesise a type when their branches synthesise consistent types. There is a dedicated rule for unannotated let bindings, which differ from function applications in a bidirectional setting due to type information flowing from the binding into the body. The typing rules satisfy graduality (§2.2).

4 Synthesis Slices↩︎

The type information of a subexpression in a bidirectional type system is derived either from within the term by synthesis, or from the surrounding context. This section defines synthesis slices which concern how to explain an expression’s synthesised type, that is, the type information internal to the expression.

4.1 Synthesis Slices↩︎

Consider a ‘program’ \(P = (\Gamma, e)\), that is, typing assumptions and an expression. When the program synthesises a type (in some type variable context \(\Delta\))⁴, all of its type information is contained within the synthesis derivation \(D \;:\; \Delta;\,\Gamma \vdash e \mathrel{{\color{BrickRed}\Rightarrow}}\tau\).

Given the derivation \(D\), we may query the type \(\tau\) by taking a slice \(\upsilon\) in \(\lfloor \tau \rfloor\). A synthesis slice is a ‘program slice’ \(\rho = (\gamma, \varsigma)\) in \(\lfloor \Gamma , e\rfloor\) which synthesises a type at least as precise as the query \(\upsilon\); this corresponds to a highlighted version of the original program.

Intuitively, \(\upsilon\) specifies the part of \(\tau\) we wish to explain; for example, querying \(\upsilon = \mathit{Int} \mathbin{\to}{\color{teal}\Box}\) for \(\tau = \mathit{Int} \mathbin{\to}\mathit{Bool}\) asks “which parts of the program account for the domain being \(\mathit{Int}\)?”. The slice might not include all the program regions relevant to the query type, but will necessarily provide a consistent subset which suffices to totally explain (independently synthesise) the query.

Many such synthesis slices exist. In particular, the original program \((\Gamma, e)\) is necessarily a synthesis slice; and for \(\mathit{SynSlice}\;D \mathbin{\blacktriangleleft} {\color{teal}\Box}\), every slice of \((\Gamma, e)\) is a valid synthesis slice. We refer to the \(\upsilon \mathrel{{\color{latticecolor}\sqsubseteq}}\phi\) condition as validity. It is intentional that this is not an exact equality, as demonstrated by the counterexample below:

4.2 Minimality↩︎

Synthesis slices provide some explanation of the query, but many are clearly useless, such as the original program itself, which corresponds to fully highlighting the program. We want to find minimal slices: those where further slicing any part of the program makes the slice invalid (synthesising a type insufficient to cover the query).

4.3 Existence of Minimal Slices↩︎

Crucially, any synthesis slice has a minimal slice below it (or is minimal):

Consequently, any derivation \(D\) has a minimal synthesis slice, as the original program is a trivial inhabitant of \(\mathit{SynSlice}\;D \mathbin{\blacktriangleleft} \upsilon\) for all \(\upsilon\).

4.3.0.1 A Brute-Force Algorithm via Graduality

The proof above is not a practical algorithm. In practice, for any term, the list of maximal slices strictly less precise than a given term can be computed efficiently by omitting exactly one leaf from the AST.

The algorithm picks the first maximal strict slice that satisfies the query and recurses; if none of the slices satisfy the query, then a minimal slice has been found, by graduality (3). This is \(\mathcal{O}(n \times T)\) where \(n\) is the program size and \(T\) the type checking complexity; type checking is linear in the program size for this calculus, so finding a minimal slice is \(\mathcal{O}(n^2)\).

See Figure [fig:syn-slice-existence] for an example lattice to descend through, stopping just before descending below the given query; all three minima are marked.

4.4 Refined Slices↩︎

In practice, the user may look at a large query \(\upsilon\) getting a large program slice \(\rho\). Therefore they may want to refine the query to focus on a subpart, \(\upsilon' \mathrel{{\color{latticecolor}\sqsubseteq}}\upsilon\), that they do not quite understand. It is always possible to pick a consistent program slice \(\rho' \mathrel{{\color{latticecolor}\sqsubseteq}}\rho\) which is a refinement of the previous slice by monotonicity (which follows from graduality, 3):

This is desirable because the user will not be shown additional information after a query refinement which would require further reasoning by the user to understand. [fig:syn-slice-refinement] illustrates a monotonic refinement path along 3 refined queries on the example lattice. If we did not follow a monotonic path during refinement we would get ‘branch hopping’:

4.4.0.1 Branch hopping.

This is where highlighted regions switch between branches when refining the query, requiring the user to switch their reasoning between the contents in each branch. For example, refining \(\upsilon = \mathbf{1}\mathbin{\to}\mathbf{1}\) to \(\upsilon' = {\color{teal}\Box}\mathbin{\to}\mathbf{1}\):

On the other hand, monotonicity does not necessarily hold in the upwards direction. Consider the \(\rho_j\) node in [fig:syn-slice-refinement], which is minimal under query \(\upsilon_0\), but no minimum for query \(\upsilon_1\) is strictly more precise than \(\rho_j\).

4.5 Decompositions↩︎

Instead of calculating slices by brute force (§4.3), it would be ideal if we could compositionally calculate minimal slices of a term from minimal subslices of its subterms. It is indeed possible to compose synthesis slices into larger synthesis slices, and we prove that all minima can be expressed by some composition; this subsection demonstrates two of the cases. We later consider how to recursively choose the compositions (§8).

4.5.1 Products↩︎

Given slices \((\gamma_1, \varsigma_1) : \mathit{SynSlice}\;D_1 \mathbin{\blacktriangleleft} \upsilon_1\) and \((\gamma_2, \varsigma_2) : \mathit{SynSlice}\;D_2 \mathbin{\blacktriangleleft} \upsilon_2\) for the two components of a pair \(D = \textrm{\mathrel{{\color{BrickRed}\Rightarrow}}\texttt{Pair}}\,D_1\,D_2\) (with synthesised types \(\phi_1, \phi_2\)), we form their product slice \((\gamma_1, \varsigma_1) \times(\gamma_2, \varsigma_2) : \mathit{SynSlice}\;D \mathbin{\blacktriangleleft} \upsilon_1 \times \upsilon_2\) by joining the two assumption slices and pairing the term slices: \[(\gamma_1, \varsigma_1) \times(\gamma_2, \varsigma_2) \;\triangleq\; (\gamma_1 \mathbin{{\color{latticecolor}\sqcup}}\gamma_2,\;(\varsigma_1, \varsigma_2))\] The pair synthesises (possibly more precise)⁵ types \(\phi_1' \times \phi_2' \mathrel{{\color{latticecolor}\sqsupseteq}}\phi_1 \times \phi_2 \mathrel{{\color{latticecolor}\sqsupseteq}}\upsilon_1 \times \upsilon_2\). For this combinator, we get the following decomposition theorem:

However, we shall later see that the converse fails: the product of two minimal slices need not be minimal, since the joined assumptions can leave one component’s term slice redundant. So one cannot simply recurse through the derivation, pairing sub-slices on \(\upsilon_1\) and \(\upsilon_2\) to obtain a minimal slice on \(\upsilon_1 \times \upsilon_2\). We explore and resolve this problem later (§8.1).

4.5.2 Let Bindings↩︎

A more subtle case is that of let-bindings, which have different assumptions for their two premises: \[\inference[\textrm{\mathrel{{\color{BrickRed}\Rightarrow}}\texttt{Let}}]{ \Delta;\,\Gamma \vdash e_1 \mathrel{{\color{BrickRed}\Rightarrow}}\tau_1 & \Delta;\,\Gamma, x:\tau_1 \vdash e_2 \mathrel{{\color{BrickRed}\Rightarrow}}\tau_2 }{\Delta;\,\Gamma \vdash \mathbf{let}\;x = e_1\;\mathbf{in}\;e_2 \mathrel{{\color{BrickRed}\Rightarrow}}\tau_2}\] A slice of a let-expression can be constructed from a slice \((\gamma_1, \varsigma_1)\) of the definition (synthesising \(\phi_1\)) and a slice \((\gamma_2, \varsigma_2)\) of the body, constrained with an assumption consistency condition: the body’s used assumptions for the bound variable \(x\) must be at most as precise as the type synthesised by the slice of the definition, \(\gamma_2(x) \mathbin{\mathrel{{\color{latticecolor}\sqsubseteq}}} \phi_1\).

Then, upon joining the assumptions for the two slices, we must remove the assumption on \(x\) from the body (notated \(\gamma_{\setminus x}\)), as this is now provided by the definition: \[(\gamma_1, \varsigma_1) \mathbin{\mathsf{def}} (\gamma_2, \varsigma_2) \triangleq (\gamma_1 \mathbin{{\color{latticecolor}\sqcup}}(\gamma_2)_{\setminus x},\; \mathbf{let}\;x = \varsigma_1\;\mathbf{in}\;\varsigma_2)\]

4.6 Contribution Slices↩︎

Finally, a minimal slice only provides an explanation; it does not show all information contributing in any way to a query type. The latter is a useful notion when performing refactors which change the type, where quickly identifying the regions of the program which rely on the old type is crucial.

Such a region can be uniquely expressed as the join of all minimal slices for the query. The contribution slice is efficient in the sense that it is a least upper bound of actual minimal slices. For this to work, synthesis slices must be closed under joins: the joined slice must also be valid:

5 Context Typing↩︎

Context typing is a novel construction for bidirectional type systems. It is inspired by one-hole contexts (zippers) of algebraic data types [27], decomposing a data structure into a focused element and its surrounding context. We apply the same idea to typing derivations: given a derivation of an expression \(e\) and focusing on a sub-term \(e'\) in \(e\), we focus on the subderivation of \(e'\) and pair it with a ‘context typing derivation’ of the surrounding context.

A context typing derivation therefore must record the extra assumptions made available at the focus by additional bound variables introduced in the captured context, and the mode of the focus (whether or not the sub-term synthesises a type). These are necessary for type checking the focus (i.e.\(e'\)) directly from the typing derivation of the context.

5.1 Context Syntax and Slice Lattice↩︎

Formally we must first define one-hole contexts on terms themselves (Figure 15). The focus of the context is notated \({\color{blue}\bigcirc}\) and is restricted to a single position in an expression. For any context, a term may be placed at the focus to produce a complete term. This is notated by \(\mathcal{C}[e]\), ‘plugging \(e\) into context \(\mathcal{C}\)’.

Precision extends to contexts, \(\mathcal{C}' \mathrel{{\color{latticecolor}\sqsubseteq}}\mathcal{C}\), additionally requiring the focus to be in the same structural position. This is required so that plugging a context preserves precision:

This lemma allows slicing to independently slice the external type information from the context and the internal type information of the focused term, whilst ensuring the whole program slice (plugging the two together) remains a valid slice of the original program.

5.2 The Context Typing Judgement↩︎

Then, we notate context typing by a judgement \(\Delta;\,\Gamma \vdash \mathcal{C}\;\mathbf{at}\;d\;\triangleright\;\Delta';\;\Gamma'\;[\,m\,]\), read as: “under assumptions \(\Delta, \Gamma\), context \(\mathcal{C}\) in a derivation of outer mode \(d\) has its focus typed under \(\Delta';\,\Gamma'\) in focus mode \(m\)”.

The outer derivation mode \(d\) records whether the whole expression \(\mathcal{C}[e]\) is in a synthesis derivation producing type \(\tau\) (\(d = \mathrel{{\color{BrickRed}\Rightarrow}}\;\tau\)) or an analysis derivation against \(\tau\) (\(d = \mathrel{{\color{BlueViolet}\Leftarrow}}\;\tau\)). The focus mode \(m\) records the type the focus \(e\) must synthesise (\(m = \mathrel{{\color{BrickRed}\Rightarrow}}\;\tau'\)), or the type it is checked against (\(m = \mathrel{{\color{BlueViolet}\Leftarrow}}\;\tau'\)). Finally, \(\Gamma'\) records the focus assumptions. Each rule in these derivations is subject to additional premises matching the corresponding term typing rules.

5.2.0.1 Example.

Consider the derivation of \(\Delta;\,\Gamma \vdash e_1(e_2) \mathrel{{\color{BrickRed}\Rightarrow}}\tau_2\) via \(\mathrel{{\color{BrickRed}\Rightarrow}}\)App, where \(\Delta;\,\Gamma \vdash e_1 \mathrel{{\color{BrickRed}\Rightarrow}}\tau\), \(\tau \mathbin{{\color{latticecolor}\sqcup}}({\color{teal}\Box}\mathbin{\to}{\color{teal}\Box}) \equiv \tau_1 \mathbin{\to}\tau_2\), and \(\Delta;\,\Gamma \vdash e_2 \mathrel{{\color{BlueViolet}\Leftarrow}}\tau_1\).

• Function position (\(e_1\) is the focus, \(\mathcal{C}= {\color{blue}\bigcirc}(e_2)\)): The corresponding context typing is: \(\Delta;\,\Gamma \vdash {\color{blue}\bigcirc}(e_2)\;\mathbf{at}\;\mathrel{{\color{BrickRed}\Rightarrow}}\;\tau_2\;\triangleright\;\Delta;\,\Gamma\;[\,\mathrel{{\color{BrickRed}\Rightarrow}}\;\tau\,]\). The focus must synthesise type \(\tau\) as per the focus mode, with the extra premises being \(\tau \mathbin{{\color{latticecolor}\sqcup}}({\color{teal}\Box}\mathbin{\to}{\color{teal}\Box}) \equiv \tau_1 \mathbin{\to}\tau_2\) and \(\Delta;\,\Gamma \vdash e_2 \mathrel{{\color{BlueViolet}\Leftarrow}}\tau_1\).

• Argument position (\(e_2\) is the focus, \(\mathcal{C}= e_1({\color{blue}\bigcirc})\)): The corresponding context typing is: \(\Delta;\,\Gamma \vdash e_1({\color{blue}\bigcirc})\;\mathbf{at}\;\mathrel{{\color{BrickRed}\Rightarrow}}\;\tau_2\;\triangleright\;\Delta;\,\Gamma\;[\,\mathrel{{\color{BlueViolet}\Leftarrow}}\;\tau_1\,]\). The focus analyses against \(\tau_1\) as per the focus mode, with the extra premises being: \(\Delta;\,\Gamma \vdash e_1 \mathrel{{\color{BrickRed}\Rightarrow}}\tau\) and \(\tau \mathbin{{\color{latticecolor}\sqcup}}({\color{teal}\Box}\mathbin{\to}{\color{teal}\Box}) \equiv \tau_1 \mathbin{\to}\tau_2\).

Specifying these rules is systematic, one for each typing rule and focus location. We give a few representative rules in Figure 16. The only additional rules are for identity contexts \(\texttt{s}{\color{blue}\bigcirc}\) and \(\texttt{a}{\color{blue}\bigcirc}\) (the base cases) where the focus mode must match the outer derivation mode.

None

Correctness of context typing is formalised via a totality theorem: every well-typed expression can be decomposed into context and expression at some focus, with a context typing matching a (consistent) typing derivation of the focused term. Conversely, a soundness theorem states that a valid context typing and expression satisfying the focus typing mode can be composed into a well-typed plugged expression.

In order to apply the same ideas as synthesis slices, we also prove a substantial static gradual guarantee (§3.3) for context typings, defining precision on modes \(m' \mathrel{{\color{latticecolor}\sqsubseteq}}m\) by lifting: \(\mathrel{{\color{BrickRed}\Rightarrow}}\,\tau' \mathrel{{\color{latticecolor}\sqsubseteq}}\mathrel{{\color{BrickRed}\Rightarrow}}\,\tau\) iff \(\tau' \mathrel{{\color{latticecolor}\sqsubseteq}}\tau\), and likewise for \(\mathrel{{\color{BlueViolet}\Leftarrow}}\). The focus mode’s class itself (analysis or synthesis) is propagated unchanged through every context typing rule.

6 Analysis Slices↩︎

With this in mind, analysis slices are simple analogues to synthesis slices, except being conducted on analysis inner mode context typing derivations. And, as the overall programs that we consider must synthesise a type, the usual analysis slices concern derivations only in synthesis outer derivation mode.⁶

Intuitively, slices of the context explain why a sub-term is expected by the surrounding context to synthesise or analyse against a given type. We typically only care about the cases where the inner mode is in analysis; a (well-typed) surrounding context does not actually influence why a term synthesises a type.⁷

6.1 Definition↩︎

Structurally, analysis slices are identical to synthesis slices (§4.1), but with expression slices \(\varsigma\) replaced by context slices \(\kappa \in \lfloor\mathcal{C}\rfloor\).

6.2 Minimality↩︎

\(\mathit{MinAnaSlice}\;\mathit{Cls} \mathbin{\blacktriangleleft} \upsilon\) is defined analogously to Definition 2, minimising over the context slice \((\kappa, \gamma)\). And as before, existence of minimal analysis slices and monotonicity follow from finiteness and graduality.

6.3 Minimally Scoped Analysis Slices↩︎

As mentioned earlier, a synthesising term derives all of its type information internally.⁸ Therefore, the type is actually only enforced by the context up until the innermost subderivation with a synthesis outer derivation mode.

For example, for an annotated term nested inside another annotation, only the inner annotation actually enforces a type on the inner term. Therefore, an algorithm need only check this region (the outer context can be fully omitted).

7 Error Marking & Type Error Debugging↩︎

This section formally applies type slicing to static error squiggles as in 3 (§1.2). It demonstrates that we can not only use this calculus to “explain types” in well-typed programs, but also effectively “explain type errors” in ill-typed programs.

This builds upon the theory of type error marking for bidirectional systems with holes of Zhao et al. [20], which we briefly recap next and extend to the type slicing core calculus (§3).

7.1 Error Marking↩︎

A marking algorithm is a pair of bidirectional judgements, \[\Delta;\,\Gamma \vdash e \looparrowright\check{e} \mathrel{{\color{BrickRed}\Rightarrow}}\tau \qquad\text{and}\qquad \Delta;\,\Gamma \vdash e \looparrowright\check{e} \mathrel{{\color{BlueViolet}\Leftarrow}}\tau,\] reading “under \(\Delta;\Gamma\), the source expression \(e\) marks to the marked expression \(\check{e}\), synthesising (resp.being analysed against) type \(\tau\)”. The marked output \(\check{e}\) has the same structure as \(e\) but wraps each point of local type failure in a mark. The marks, representing highlighting an entire erroneous term \(e\), are tabulated in 1 alongside the corresponding typing rule failures.

The core calculus studied gives rise to four classes of errors: type inconsistencies when subsumption cannot be applied, shape errors when rules expect a sub-term to join (match) a specific type shape, mode limitations where syntax which cannot synthesise its type is expected to provide type information; and variable scoping errors, which do not pertain to types and so cannot be debugged by type slicing.

Importantly, marked terms can be type-checked by treating the marks as ‘non-empty’ holes, synthesising \({\color{teal}\Box}\) (and recursively marking and type-checking the inner term).

The validity of this method is formalised by two theorems: totality ensures marks account for every possible typing error, and erasure ensures adding marks does not change a term’s structure.

7.2 Marked Context Typing↩︎

In this style, we extend context typing (§5) to marked context typing \(\Delta;\,\Gamma \vdash \mathcal{C} \looparrowright\check{\mathcal{C}}\;\mathbf{at}\;p\;\triangleright\;\Delta';\,\Gamma'\;[\,m\,]\), threading a marked context \(\check{\mathcal{C}}\) alongside \(\mathcal{C}\) (with context marks defined analogously to expressions), adding one error rule per mark form of 1. We have proven analogous totality and soundness theorems hold for marked contexts, mirroring the unmarked plug decomposition and composition (6 7).

7.3 The Debugging Recipe by Example↩︎

We may now relate the tools developed over the last four sections to explain type errors:

1. Place the focus (cursor) at some marked term. This splits the marked program into a marked context \(\check{\mathcal{C}}\) and marked focus \(\check{e}\), with \(\check{\mathcal{C}}[\check{e}]\) recovering the program; a marked context typing at the focus is then derivable by totality of marked context typing.

2. Synthesis slice the internal type information, the term at the focus, \(\check{e}\), if the focus mode \(m\) is in synthesis (\(\mathrel{{\color{BrickRed}\Rightarrow}}\;\tau\)).

3. Analysis slice the external type information, the context typing itself, if the focus mode \(m\) is in analysis (\(\mathrel{{\color{BlueViolet}\Leftarrow}}\;\tau\)).

4. Pick queries to explore the error. For type-inconsistency marks both the synthesis and analysis slices exist (two context typings exist from step 1). From these, only the inconsistent parts need be queried to explain the error. For shape errors, simply query just the outermost shape of the synthesised type; mode-limitation errors are analogous on the analysis side.

We give some worked examples, notating with a , a NavyBlueOliveGreen NavyBlueteal , and/or an OliveGreenOliveGreen OliveGreenteal . ‘Purely structural’ slice regions which do not add or manipulate type information (i.e. bindings) are in a lighter shade.

7.3.1 Type inconsistency: \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\tau' \not\sim \tau}\)↩︎

Consider the program \[\mathbf{let}\;p : 1 \mathbin{\to}1 = (\texttt{true},\,\texttt{false})\;\mathbf{in}\;p.\] The RHS \((\texttt{true},\,\texttt{false})\) synthesises \(\texttt{Bool} \times \texttt{Bool}\) but is analysed against \(1 \mathbin{\to}1\). Marking inserts \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\texttt{Bool} \times \texttt{Bool} \not\sim 1 \mathbin{\to}1}\) around the RHS: \[\mathbf{let}\;p : 1 \mathbin{\to}1 = \tikz[baseline=(N.base)]{ \node[draw=BrickRed!85, line width=0.7pt, rounded corners=2pt, inner sep=2pt, fill=BrickRed!6, anchor=base] (N) {\strut{{\color{markcolor}\llparenthesis}(\texttt{true},\,\texttt{false}) {\color{markcolor}\rrparenthesis}}_{\texttt{Bool} \times \texttt{Bool} \not\sim 1 \mathbin{\to}1}}; } \;\mathbf{in}\;p.\] Marking would ordinarily report the error \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\texttt{Bool} \times \texttt{Bool} \not\sim 1 \mathbin{\to}1}\) with the entire term highlighted. However, in reality, only the outermost type constructors are actually causing the (initial) type inconsistency, and type slicing allows query refinements of the full types. In full:

7.3.1.1 Decomposition

The (context, focus) pair the marking factors into is \[\mathcal{C} \;=\; \mathbf{let}\;p : 1 \mathbin{\to}1 = {\color{blue}\bigcirc}\;\mathbf{in}\;p, \qquad e \;=\; (\texttt{true},\,\texttt{false}),\] with the focus at \(\mathrel{{\color{BlueViolet}\Leftarrow}}\,(1 \mathbin{\to}1)\). The two debugging queries run on the two sides of this split.

7.3.1.2 Synthesis Slice

\(\mathit{MinSynSlice}\) at the minimal type-slice \(\upsilon \mathrel{{\color{latticecolor}\sqsubseteq}}\texttt{Bool} \times \texttt{Bool}\) that still witnesses \(\upsilon \not\sim (1 \mathbin{\to}1)\): \[e \;\rightsquigarrow\; (\,\texttt{true}\, \def OliveGreen{NavyBlue} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=NavyBlue!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=NavyBlue!12, anchor=base] (N) {\strut,}; } \,\texttt{false}\,) \qquad\text{with}\qquad \upsilon = {\color{teal}\Box}\,{\times}\,{\color{teal}\Box}.\]

7.3.1.3 Analysis Slice

\(\mathit{MinAnaSlice}\) at the minimal \(\psi \mathrel{{\color{latticecolor}\sqsubseteq}}1 \mathbin{\to}1\) that still witnesses \((\texttt{Bool} \times \texttt{Bool}) \not\sim \psi\): \[\mathcal{C} \;\rightsquigarrow\; \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut\mathbf{let}}; } \;p\, \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut:}; } \,1\, \def OliveGreen{OliveGreen} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!12, anchor=base] (N) {\strut\mathbin{\to}}; } \,1\, \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut=}; } \,{\color{blue}\bigcirc}\, \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut\mathbf{in}}; } \;p \qquad\text{with}\qquad \psi = {\color{teal}\Box}\,{\mathbin{\to}}\,{\color{teal}\Box}.\]

7.3.1.4 Full view:

The slices pick out exactly what each side contributes to the failure.

\[\tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut\mathbf{let}}; } \;p\, \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut:}; } \,1\, \def OliveGreen{OliveGreen} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!12, anchor=base] (N) {\strut\mathbin{\to}}; } \,1\, \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut=}; } \, \tikz[baseline=(N.base)]{ \node[draw=BrickRed!85, line width=0.7pt, rounded corners=2pt, inner sep=2pt, fill=BrickRed!6, anchor=base] (N) {\strut{{\color{markcolor}\llparenthesis}(\,\texttt{true}\, \def OliveGreen{NavyBlue} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=NavyBlue!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=NavyBlue!12, anchor=base] (N) {\strut,}; } \,\texttt{false}\,) {\color{markcolor}\rrparenthesis}}_{\texttt{Bool} \times \texttt{Bool} \not\sim 1 \mathbin{\to}1}}; } \, \tikz[baseline=(N.base)]{ \node[draw=OliveGreen!25, dashed, line width=0.4pt, rounded corners=1.5pt, inner sep=1.5pt, fill=OliveGreen!4, anchor=base] (N) {\strut\mathbf{in}}; } \;p.\]

We can see that this recipe does not arbitrarily blame either the synthesising term or the analysing context for the error; after all, errors are commonly in annotations, especially when assigning types in a gradual language (49%) [21].

However, type slicing is flexible. A user who does want to trust the surrounding context (annotations), as is often done in conventional type error highlighting, can simply only query the synthesis-side. Or vice versa, to trust the implementation, which is useful when refactoring code to a different type, which conflicts with existing annotations.

7.3.2 Shape mismatches: \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\blacktriangleright \mathbin{\to}}\), \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\blacktriangleright +}\), \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\blacktriangleright \times}\), \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\blacktriangleright \forall}\)↩︎

The shape-mismatch marks all occur in similar situations: the syntactic position of the focus requires a type kind, but the focus’s synthesised type does not match this.

7.3.3 Unannotated Lambda against Non-Arrow: \({{\color{markcolor}\llparenthesis}\cdot {\color{markcolor}\rrparenthesis}}_{\sim \mathbin{\to}}\)↩︎

Unannotated lambdas \(\lambda y.\,e\) have no synthesis rule; their type can only be determined by the surrounding context. Consequently it has no synthesis type, so type inconsistencies are not marked via subsumption, but instead by a mode limitation mark. In this situation all the relevant type information is derived from the surrounding context, so we use analysis slices.

7.3.4 Unbound variable: \({\color{markcolor}\langle} k {\color{markcolor}\rangle}\!\mathrel{{\color{BrickRed}\Rightarrow}}\)↩︎

The free-variable mark records a scope failure. There are no types involved, so type slicing is inapplicable.

8 Optimising Type Slice Calculation↩︎

The theory of synthesis and analysis slices (§4, §6) establishes which slices exist, and provides a brute-force algorithm. This section explores these structures further to improve the brute-force algorithm.

8.1 Products of Synthesis Slices↩︎

We earlier suggested recursively calculating minimal slices of subterms and composing them together (§4.5). However, this cannot be done naively: the product of two minimal slices is not necessarily minimal. Consider the following if statement: \[\Gamma = (x \mathbin{:} \mathbf{1} \mathbin{\to}\mathbf{1},\; y \mathbin{:} \mathbf{1} \mathbin{\to}\mathbf{1}), \qquad e = \mathbf{if}\;\mathbf{true}\;\mathbf{then}\;x\;\mathbf{else}\;y, \qquad \tau = \mathbf{1} \mathbin{\to}\mathbf{1},\] and ask for slices of \(D : \Delta;\,\Gamma \vdash e \mathrel{{\color{BrickRed}\Rightarrow}}\tau\) at the full query \(\upsilon = \mathbf{1} \mathbin{\to}\mathbf{1}\). There are four incomparable minimal full slices, displayed together as underlines:

(A)

Both branches are retained; the assumption slice keeps \(x\)’s domain only and \(y\)’s codomain only (joining to \(1 \mathbin{\to}1\)).

(B)

Symmetric to (A), taking the opposite choices for the assumption slice

(C)

Else-branch omitted.

(D)

Symmetric to (C): then-branch omitted.

Slices (A) and (B) are minimal because each variable is sliced differently across the two uses, and none are program slices of each other. However, notice that (A) and (B) are not subslices of the product with \(x\), where only 2 minima exist:

When this expression is embedded in the product \((\mathbf{if}\;\mathbf{true}\;\mathbf{then}\;x\;\mathbf{else}\;y,\; x)\), the two assumptions are joined. However, the right projection’s use of \(x\) is strictly stronger than that of slices (A), (B), and (D); we are aliasing this variable’s assumption. Slices (A) and (B) are no longer minimal under this aliased assumption, meaning they are not subslices of the overall product. Slice (D) is still valid because it does not actually use \(x\).

8.2 Term-Minimal Slices↩︎

To rule out slices like (A) and (B) (§8.1), we strengthen the notion of slices. We first calculate the minimal expression under maximal typing assumptions, and then minimise the assumptions afterwards. By graduality, this is a minimal synthesis slice.

Minimality lifts directly from the slice lattice on \(e\) alone, and existence and monotonicity follow analogously to synthesis slices (4 5).

Crucially, the two notions of minimality do not coincide: term-minimality is strictly stronger. Not all minimal slices are term-minimal under maximal assumptions.

8.3 Calculating Term-Minimal Slices↩︎

The rest of this section develops a structural calculus that characterises minimal term slices via a judgement: \[\Gamma \vdash e \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \tau \mathbin{\blacktriangleleft} \upsilon \;{\color{BrickRed}\rightsquigarrow}\; \varsigma \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \psi \dashv \gamma,\] read “the typing \(\Gamma \vdash e \mathrel{{\color{BrickRed}\Rightarrow}}\tau\) at query \(\upsilon\) produces term slice \(\varsigma\), synthesises \(\psi\), and uses assumptions \(\gamma\)”. The fourth output \(\gamma\) is a minimal assumption slice to retrieve a minimal slice corresponding to the term-minimal slice.

The cases that deserve commentary are products, the binding constructs, function application, and type application.

8.3.1 Products↩︎

With term minimality, we now have that two minimal synthesis slices which are also term-minimal can be composed into a term-minimal, minimal synthesis slice. For a query \(\upsilon_1\times \upsilon_2\) on the product, the projections are queried with \(\upsilon_1\) and \(\upsilon_2\) individually:

\[\inference[\textrm{\mathrel{{\color{BrickRed}\Rightarrow}}\texttt{Pair}}]{ \Delta;\,\Gamma \vdash e_1 \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \tau_1 \mathbin{{\color{BrickRed}\blacktriangleleft}} \upsilon_1 \;{\color{BrickRed}\rightsquigarrow}\; \varsigma_1 \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \psi_1 \,\dashv\, \gamma_1 & \Delta;\,\Gamma \vdash e_2 \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \tau_2 \mathbin{{\color{BrickRed}\blacktriangleleft}} \upsilon_2 \;{\color{BrickRed}\rightsquigarrow}\; \varsigma_2 \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \psi_2 \,\dashv\, \gamma_2 }{ \Delta;\,\Gamma \vdash (e_1, e_2) \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \tau_1 \times \tau_2 \mathbin{{\color{BrickRed}\blacktriangleleft}} \upsilon_1 \times \upsilon_2 \;{\color{BrickRed}\rightsquigarrow}\; (\varsigma_1, \varsigma_2) \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \psi_1 \times \psi_2 \,\dashv\, \gamma_1 \mathbin{{\color{latticecolor}\sqcup}}\gamma_2 }\]

8.3.2 Function Application↩︎

All the synthesised type information from a function application is derived from the function itself. We may simply omit the argument, and slice the function by \({\color{teal}\Box}\mathbin{\to}\upsilon\): \[\inference[\textrm{\mathrel{{\color{BrickRed}\Rightarrow}}\texttt{App}}]{ \Delta;\,\Gamma \vdash e_2 \mathrel{{\color{BlueViolet}\Leftarrow}}\tau_1 & \upsilon \neq {\color{teal}\Box} & \Delta;\,\Gamma \vdash e_1 \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \tau_1 \mathbin{\to}\tau_2 \mathbin{{\color{BrickRed}\blacktriangleleft}} {\color{teal}\Box}\mathbin{\to}\upsilon \;{\color{BrickRed}\rightsquigarrow}\; \varsigma_{\mathit{fn}} \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \psi_1 \,\dashv\, \gamma }{ \Delta;\,\Gamma \vdash e_1\,e_2 \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \tau_2 \mathbin{{\color{BrickRed}\blacktriangleleft}} \upsilon \;{\color{BrickRed}\rightsquigarrow}\; \varsigma_{\mathit{fn}}({\color{teal}\Box}) \mathbin{\mathrel{{\color{BrickRed}\Rightarrow}}} \mathsf{cod}(\psi_1) \,\dashv\, \gamma }\]

8.3.3 Binding Constructs↩︎

Rules which bind variables are more complex, as they abstract a variable used in the minimised body. The general method is to slice them by first slicing the body, extracting the assumption it needed on the bound variable from the minimal assumptions \(\gamma\), then slice the definition / type annotation using this.

Notice that this is the opposite direction to typechecking, e.g. let bindings type the definition first, then use the result to type the body, but slicing slices the body first to determine the minimal assumption to slice the definition with.

8.3.4 Type Application↩︎

Type application works by matching the type function’s type against the query to collect a list of constraints on the type variable, the join of which gives the sliced type argument \(\hat{\sigma}\). The type function is then sliced with a matched query \(\widehat{\upsilon}\), where each position corresponding to the type variable \(\alpha\) in the type function’s type is replaced by \(\alpha\) itself and other positions are carried over from the query unchanged. Figure 23 illustrates the construction on a query whose two subparts are matched with an \(\alpha\) with differing constraints.

8.4 Case Expressions↩︎

The case rule is the difficult one, appearing to require an iterative fixed point algorithm. This is because the two branch types join to produce the resulting type which is being queried upon. As synthesis slices are not exact, a query may be split into two disjoint types, yet a minimal slice of one branch may produce a more precise type than the query (overflow), which is also produced by a sibling branch. The sibling branch may then admit further slicing, as it no longer needs to provide this redundant part of the type. Lack of an upwards version of monotonicity ([fig:syn-slice-refinement]) makes this difficult to solve in general without brute force.

However, when the branch slices exactly synthesise disjoint type queries, then there is no redundancy and the result is minimal. The scrutinee can be sliced using the join of the minimal assumptions on the branches, much like with let bindings.

To express disjoint types we can use co-Heyting subtraction \(\upsilon_1 \mathbin{{\color{latticecolor}\setminus}}\upsilon_2\), which is the least slice whose join with \(\upsilon_2\) recovers \(\upsilon_1\), i.e. “the part of \(\upsilon_1\) not already covered by \(\upsilon_2\)”, e.g. \(\def OliveGreen{NavyBlue} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=NavyBlue!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=NavyBlue!12, anchor=base] (N) {\strut1 \times 1}; } \;\mathbin{{\color{latticecolor}\setminus}}\; \def OliveGreen{NavyBlue} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=NavyBlue!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=NavyBlue!12, anchor=base] (N) {\strut1 \times}; } \,{\color{teal}\Box}\;=\; {\color{teal}\Box}\, \def OliveGreen{NavyBlue} \def densely dashdotted{dashed} \ifx OliveGreenOliveGreen\def densely dashdotted{dotted}\fi \ifx OliveGreenteal\def densely dashdotted{densely dashdotted}\fi \tikz[baseline=(N.base)]{ \node[draw=NavyBlue!60, densely dashdotted, line width=0.5pt, rounded corners=1.5pt, inner sep=1.5pt, fill=NavyBlue!12, anchor=base] (N) {\strut\times 1}; }\).

Then, a disjoint cover of query \(\upsilon\) is one such that \(\upsilon\mathbin{{\color{latticecolor}\setminus}}\upsilon_1 = \upsilon_2\) and \(\upsilon \mathbin{{\color{latticecolor}\setminus}}\upsilon_2 = \upsilon_1\). The case expression will necessarily synthesise \(\upsilon_1 \mathbin{{\color{latticecolor}\sqcup}}\upsilon_2\) which equals \(\upsilon\) by standard co-Heyting algebra rules. Note that the lattice is not a boolean algebra, so \(\upsilon_1 \mathbin{{\color{latticecolor}\sqcap}}\upsilon_2 \neq {\color{teal}\Box}\) in general.

The Hazel implementation simply does a disjoint split and ignores the overflow issue to work in linear time complexity. This is why it is an approximation. But, it is perfectly feasible to use this approximation and then continue with the brute force algorithm, as we expect the approximation to be very close to the minimum in almost all cases. Further, as overflow only occurs due to variable aliasing, the brute force search need only consider aliased variables at the leaves.

8.5 Calculating Analysis Slices↩︎

Analysis slices are calculated directly from synthesis slices. The only rule that creates a type checking judgement is function application. Consider the analysis slice of a function argument with query type \(\upsilon_1\); it is just the function application and a slice of the function under \({\color{teal}\Box}\to \upsilon_1\). That is, to explain why a function argument must be a given type, we ask why the corresponding function has that type as its domain.

However, to recursively calculate the analysis slice of an application when the focus is deep inside the argument, the analysis slice of the argument itself must be calculated, but its outer derivation mode is in analysis. The analysis slices defined earlier (§6.1) do not apply here.

We need an additional notion of inner analysis slices. Dually to regular (outer) analysis slices, which treat the synthesis mode as an input, the inner slices treat the analysis derivation mode as an output, and attempt to minimise it.

Intuitively, an inner analysis slice gives the minimal assumptions, context, and additionally the minimum analysis type to be imposed on it by the outer context, such that the queried analysis type holds at its focus. In particular, slicing the function in an application would use this minimal outer analysis mode type on the argument to slice the domain type of the function.

A minimal inner analysis slice minimises the whole triple, \(\upsilon_{\mathrm{outer}}\) included (so that an application slices the function’s domain by no more than the argument requires).

9 Full Type Slices – Slicing Assumption Definitions↩︎

Synthesis slices are explained using a set of minimal assumptions. However, in real code, these are actually provided by the surrounding context (or from external code). Providing these minimal assumptions via a full slice of this context can be very meaningful. For example, when debugging a type error, the error itself may be non-local, within a variable definition elsewhere, giving one of the used variables the wrong type. In this situation the error is in the definition, and we could debug it by inspecting (and slicing) that definition.

A full type slice is a fully sliced decomposition of a program around a focus, which can be pieced back together to form a well-typed program with the same (or stronger) typing properties at the focus as some given query:

Importantly, the pair of slices forms a well-typed program: by context typing soundness, \(\kappa[\varsigma]\) synthesises \(\psi\). Then, a minimal type slice is one in which the context \(\kappa\) and the focused expression \(\varsigma\) are jointly minimised alongside minimal external typing assumptions of the context typing \(\gamma\). Notably, we do not minimise the assumptions to the focused term, as its assumptions are now explicitly provided by the surrounding context (and \(\gamma\)).

As slices can be inexact, efficiently calculating a minimal context providing sufficient assumptions to a minimal SynSlice at the focus is non-trivial. The Hazel implementation instead closely approximates this by slicing the definition / annotation on each binding by its required type as per the minimal assumptions of the focused term. When each slice of these definitions is exact, the resulting type slice is minimal.

For terms in analysis mode, the full type slice is just the analysis slice, as the empty focus (with type \({\color{teal}\Box}\)) analyses successfully against any type.

10 Minimum-Size Slices↩︎

Minimal slices are not unique, and some are actually larger than others in the sheer number of terms highlighted. So, one might rank them by size: the number of highlighted positions, asking for a minimum-size slice. For this core calculus, finding such a slice is NP-hard in general. This implies that an algorithm attempting to also reduce the absolute size of slices should use heuristics to avoid or reduce the likelihood of cases with exponential time complexity.

We can construct a reduction from the NP-hard set cover optimisation problem as follows, and shown in 24:

• Encode a universe \(U = \{1,\dots,n\}\) as a type \(\tau = 1 \times \cdots \times 1\) (\(n\) factors, one position per element)

• Encode each of \(m\)-many sets \(S_j\) in the set cover problem by an assumption \(x_j : T_j \mathrel{{\color{latticecolor}\sqsubseteq}}\tau\) in \(\Gamma\) with \(T_j\) defined by the \(i\)th projection of \(T_j\) being \(1\) if and only if \(i \in S_j\).

• Construct a case tree with empty scrutinees and placing all \((x_j, I_j)\), defining \(I_j\) as the \(m\)-ary product with \(j\)th projection being \(1\) and all others \({\color{teal}\Box}\).

Then, if a synthesis slice is queried on this case tree with \(\tau \times 1 \times \dots \times 1\), each \(I_j\) must be retained, so the whole tree structure must be retained, and the only variance in the size of the slices is purely dependent on which variables \(x_j\) were retained.

As we queried \(\tau\) in the first projection then \(\bigsqcup_{j=1}^m{T_j} = \tau\), which implies there are \(m\) subsets⁹ \(S_j' \subseteq S_j\) such that \(\bigcup_{j=1}^mS'_j = U\). Hence, the retained \(S_j\) form a set-cover. Finally, the only variance in the size of the slice was in the number of variables \(x_j\) chosen, i.e. the number of sets chosen; hence, a minimum-size synthesis slice corresponds to a minimum set cover.

11 Related Work↩︎

Program slicing methods have been explored extensively, in various forms and for many applications [28]. Here we compare type slicing with these, being loosely related in foundation to Galois slicing [2], and in application to type error slicing [7], [8], before relating to the broader type debugging literature (§11.5).

11.1 Classical Program Slicing↩︎

Classical program slicing [28] was first introduced by Weiser [29]. Here, a slice is a subprogram preserving the value of a chosen variable at a chosen program point: a ‘criterion’. Similarly to type slicing, the subprogram is a syntactically well-formed program which can be analysed (evaluated). The criterion is superficially similar to type slicing queries, with two significant differences. First, a type query is itself a slice of a type, which has compound structure, rather than a set of plain variables. Second, type slices cannot in general preserve all queries exactly ([lem:exact-not-exist]), so we ask only for validity (8), which remains a ‘sufficient’ explanation.

Classical slicing distinguishes static slices (preserved over all executions) from dynamic slices (over one fixed execution) [30]. Type slicing can be viewed as a dynamic slicing method, as it fixes a particular typing derivation; however, most type systems, including ours, have no non-trivial non-determinism, making this distinction largely irrelevant.

11.2 Galois Slicing↩︎

Galois slicing [2] is a lattice-theoretic approach to dynamic program slicing that has been applied and related to a wide range of calculi and user interfaces [3]–[6]. Type slicing shares the foundational use of lattices and precision, but differs decisively in the lack of a Galois connection.

In Perera’s setting, a program evaluation lifts to a meet-preserving map \(\mathit{eval}_{\rho,e} : \lfloor \rho, e\rfloor \to \lfloor v\rfloor\) between the slice lattices of partial programs and partial values. By an adjoint functor theorem [26], such a map is the upper adjoint of a unique Galois connection, whose lower adjoint \(\mathit{uneval}\) is the ‘backward slice function’ sending a partial-value query to a least program slice evaluating to it.

For total type systems assigning unique types like the core calculus (§3), the natural type-slicing analogue of \(\mathit{eval}_{\rho,e}\) maps partial assumptions and expressions to partial types by type checking. \[\phi_D : \lfloor \Gamma, e \rfloor \to \lfloor \tau \rfloor\]

However, this ‘forward map’ \(\phi_D\) is not meet-preserving in general. Consider \(D : \Delta;\,\Gamma \vdash (\mathbf{case}\;e\;\mathbf{of}\;x_1.\,e_1 \mid x_2.\,e_2) \mathrel{{\color{BrickRed}\Rightarrow}}\tau\) in which both branches independently synthesise the same type \(\tau \mathrel{{\color{latticecolor}\sqsupset}}{\color{teal}\Box}\), and take the two slices \(s_1\) keeping only the first branch and \(s_2\) keeping only the second. Both are defined, yielding \(\phi_D(s_1) = \phi_D(s_2) = \tau\), but their meet \(s_1 \mathbin{{\color{latticecolor}\sqcap}}s_2\) omits both branches, giving \(\phi_D(s_1 \mathbin{{\color{latticecolor}\sqcap}}s_2) = {\color{teal}\Box}\neq \tau = \phi_D(s_1) \mathbin{{\color{latticecolor}\sqcap}}\phi_D(s_2)\).

11.3 Type Error Slicing↩︎

Type error slicing, like type slicing, is a static analysis on a typing problem. Both share the broad goal of attributing type-level information back to source positions, but differ in language target, the underlying mathematical structure, and the scope.

Wand [7] and Haack and Wells [8] work in a globally inferred Hindley-Milner system; the program is reduced to a system of equality constraints over type variables. Wand’s instrumented unification reports the constraint sites contributing to a failure, with no minimality guarantee; Haack and Wells compute a type error slice as a minimal unsatisfiable subset of the constraint set, projected back to the corresponding minimal subset of source positions. Skalpel [31] matures and scales this approach to Standard ML, and the Chameleon debugger [32] underlines the same minimal location sets interactively.

These slices are not structure-preserving programs but flat sets of constraints and sources, so the results cannot themselves be type checked or executed. Tip and Dinesh [9] are the exception: slicing explicitly typed languages by dependence tracking in a rewriting-based checker, their slices are programs guaranteed to reproduce the same error when type checked.

The scope also differs: type error slicing answers “why does this program fail to type-check?”, whereas type slicing answers “why does this expression have this type?”. Via marking (§7) [20], which elaborates every well-formed expression into a totally typed derivation, type slicing applies also to ill-typed programs. So, here, the question of “why this type?” subsumes “why this fails to type-check?”.

11.4 Type-Directed Slicing↩︎

[10] recently independently introduced type-directed slicing, implemented for Java in the tool Specimin. Their motivation and application is more specific than ours: their slices serve the maintainers of a typechecker, reducing a large program exhibiting a known bug to a small test case reproducing it.

Given a target program element and a typechecker specified by its type rules, a type-directed slicer statically computes a smaller program on which the typechecker behaves identically at the target: essentially type slicing restricted to maximal queries (no partial queries). However, the approach, theory, and proofs differ greatly, as do the languages considered, with ours extending to bidirectionally inferred types, applying to programs with fewer annotations and better support for first-class functions. On the other hand, their work applies in practice to a wider range of analyses, including exceptions, crashes, and nullness analysis.

Their work was empirically evaluated on historical bugs of javac, NullAway [33], and the Checker Framework [34], suggesting our theory is similarly applicable to such real world use cases; conversely, partial queries may be a worthwhile extension to their tools, especially when a type checker produces multiple cascading bugs.

11.5 Type Debuggers & Type Explanation↩︎

Beyond slicing, there is a broad literature on explaining, localising, and repairing type errors. The oldest line explains types: Beaven and Stansifer [35] and Duggan and Bent [36] generate textual explanations from instrumented unification, [37] explain inferred polymorphic types of well-typed programs, and [17] navigates compositional explanation graphs via algorithmic debugging. These systems answer the same question as a synthesis slice—why does this term have this type?—but produce prose or inference traces, whereas a type slice is itself a minimal well-formed program that can be re-checked and further refined. Interactive debuggers similarly answer such queries: Chameleon [32] over a constraint store for Haskell, reporting errors as minimal location sets as in §11.3, and Argus [38] for Rust trait errors in the IDE.

A larger body of work improves error reports for globally inferred languages: constraint-solving heuristics in Helium [39], ranking likely error causes over constraint graphs [13], [40], minimum error sources via MaxSMT [14], [41], black-box correcting sets [42], subtyping-constraint flow messages [43], dynamic witnesses [44], and learned localisation [45] and repair [46]. These techniques answer “where is the error?” or “how might it be fixed?” rather than “why this type?”; empirically, most type errors implicate multiple program points [47], which type slicing surfaces directly.

As slices are themselves programs, these tools compose with type slicing (§1).

12 Further Extensions & Applications↩︎

12.1 Set-Theoretic Types↩︎

Type slicing looks especially promising for common gradual type systems in which control flow and types are intertwined: an expression’s type depends non-trivially on the branches inside a function, or the control-flow path in which the expression lies. Explaining a type then genuinely requires considering the branches within the code, rather than just annotations and literals; as type slices necessarily retain program structure, they can retain the appropriate control flow structure.

Set theoretic types extend the type language with union, intersection, and negation, letting a term carry several types simultaneously, typing overloaded functions and typecase constructs common in real world hybrid typed languages (e.g.TypeScript, or Elixir [48]). Relevant foundations, including graduality proofs, have been explored [49]–[51], ready for type slicing to build upon.¹⁰

To demonstrate this application, consider generalising sum types of the core calculus (§3) to allow sum injections to synthesise partially dynamic types: when \(\Delta;\,\Gamma \vdash e \mathrel{{\color{BrickRed}\Rightarrow}}\tau\), let \(\Delta;\,\Gamma \vdash \iota_1\; e \mathrel{{\color{BrickRed}\Rightarrow}}\tau + {\color{teal}\Box}\) and \(\Delta;\,\Gamma \vdash \iota_2\; e \mathrel{{\color{BrickRed}\Rightarrow}}{\color{teal}\Box}+ \tau\). Then an if statement \(\mathit{pred} \triangleq \mathbf{if}\;x > 0\;\mathbf{then}\;\iota_1(x - 1)\;\mathbf{else}\;\iota_2(())\) synthesises a sum type \(\mathbb{N} + 1\) without requiring annotations, much as union type inference works (i.e. union type \(\mathbb{N}\;|\;1\)), and type slicing can explain where each component comes from: querying \({\color{teal}\Box}+ 1\) highlights exactly the failing branch, and \(\mathbb{N} + {\color{teal}\Box}\) the succeeding one. We mechanised this example.

12.2 Occurrence Typing↩︎

Occurrence typing [52] is another common technique in hybrid type systems. Inside the true branch of if (typeof x = int) ... else ..., the type of x is refined as an int. These explicitly require exploring the surrounding control flow, which can be extensive, to reason about the types. As type slices necessarily retain program structure, they can provide a reduced slice with minimal control flow to reason within. Formally applying type slicing to such systems will, however, need extensive integration work with bidirectional typing and static graduality.

12.3 Implicit Polymorphism↩︎

Globally inferred languages have much more confusing typing derivations and errors than locally inferred ones, so extending the calculus to implicit polymorphism would expand the application significantly. Explaining even well-typed code is particularly useful here: error marks are often mis-localised, leaving the real error in well-typed code whose types conflict with the programmer’s expectation. Adapting the constraint slicing of Wand [7] and Haack and Wells [8] to integrate with type slicing is worth exploring.

12.4 Cast Slicing & Dynamics↩︎

However, slices are no longer slices of the original program once dynamic reductions are performed. Tracking dynamic execution, perhaps integrating ideas from Perera [2], [4], would allow tracing casts back to source with stronger guarantees; dynamic slices measurably aid diagnosis of run-time type errors in gradual languages [53].

13 Conclusions↩︎

This paper formulated type slicing theory for a bidirectional calculus with explicit System F polymorphism, bindings, products, and sums, mechanised in Agda, and formally integrated it with the error-marking calculus of [20], applying it to ill-typed programs and justifying its sound use in debugging all static type errors. This positions type slicing as a promising tool for practical languages, especially gradually typed ones, explaining both static and, in follow-up work, dynamic types.

References↩︎

---

1. Folding all other branches into a single fold projector is not currently supported by the Hazel UI, but is shown here for illustrative purposes.↩︎

2. Hence the name.↩︎

3. Typically notated \(\tau \blacktriangleright \tau_1 \mathbin{\to}\tau_2\).↩︎

4. Type variable contexts are not sliced as the only information such slices would encode is whether a type variable was used, which can be extracted purely syntactically from the resulting slice. Typing assumptions are different because we can partially require an assumption.↩︎

5. Due to \(\gamma_1 \mathbin{{\color{latticecolor}\sqcup}}\gamma_2\) being larger than \(\gamma_1\) and \(\gamma_2\).↩︎

6. An extension to analysis outer modes, which is useful for efficient calculation, is discussed later.↩︎

7. A context may define a variable which is used in a synthesising term, non-locally affecting the subterm’s type. However, assumption slices are treated entirely separately in both modes. That is, we do not ask the analysis slice to explain how exactly the bindings provide the minimal assumptions for the focus, only how it explains the type at the focus.↩︎

8. Again, given that assumptions are tracked externally.↩︎

9. Subsets, as a minimal slice can use less precise assumptions \(x_j\), i.e. \(x_j : T'_j \mathrel{{\color{latticecolor}\sqsubseteq}}T_j\)↩︎

10. After adapting into a bidirectional setting with expression holes.↩︎