Development tools report what type an expression has, but not why it has that type. This project develops a theory of type slicing: a programmer selects a term, queries any part of its type information, and receives a program slice that is sufficient to reproduce the queried type. We formulate type slicing for bidirectional type systems, where synthesis slices explain the type a term synthesises and analysis slices explain the type expected by its surrounding context.
The theory applies to any bidirectional system equipped with precision orders on types and terms satisfying a downwards static graduality property. The metatheory is developed over a core calculus with holes, products, sums, and explicit polymorphism, based on the Hazelnut and marked lambda calculi. Every query has a minimal slice, and refining a query monotonically shrinks its minimal slices; these slices can be calculated both exactly and approximately. Integrating type slicing with error marking theory extends these results to arbitrary ill-typed programs, so a single mechanism explains both types and type errors in complete, incomplete, and erroneous code.
1 Links
The project was completed as Max Carroll's Part III project, following on from his earlier Part II work on gradual type error debugging. The metatheory is mechanised in Agda, and a linear-time approximation of type slicing is implemented for the Hazel programming environment.
The writeup is available as a preprint on arXiv or here.