Search papers, labs, and topics across Lattice.
This paper introduces a novel theory of bidirectional type slicing, enabling programmers to query specific parts of type information and receive a corresponding program slice that reproduces the queried type. The authors establish a metatheory over a core calculus, proving that every query has a minimal slice and that refining queries leads to smaller slices, thereby enhancing the understanding of type synthesis and expected types in programming contexts. Additionally, the integration of type slicing with error marking theory allows for a unified explanation of types and type errors in both well-typed and ill-typed programs, with practical implementation in the Hazel programming environment.
Every type query can be answered with a minimal program slice, transforming how developers understand and debug type information in their code.
Development tools report what type an expression has, but not why it has that type. This paper 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. We develop the metatheory over a core calculus with holes, products, sums, and explicit polymorphism, based on the Hazelnut and marked lambda calculi. We prove that every query has a minimal slice and that refining a query monotonically shrinks its minimal slices. We then show how to calculate these slices both exactly and approximately. Finally, 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. The metatheory is mechanised in Agda, and a linear-time approximation of type slicing is implemented for the Hazel programming environment.
