# Bidirectional Type Slicing

*2026-07-01 — paper*

Authors: Max Carroll, Anil Madhavapeddy, Cyrus Omar


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.


DOI: 10.48550/arXiv.2607.12197
Classification: preprint
Venue: arXiv
URL: http://arxiv.org/abs/2607.12197

## Related

- [.plan-26-29: Perfect weather, imperfectly measured, precisely predicted](https://anil.recoil.org/notes/2026w29) (note, 2026-07-19)
- [.plan-26-28: What fun papers piled up while I was out at sea](https://anil.recoil.org/notes/2026w28) (note, 2026-07-12)
- [Bidirectional type slicing](https://anil.recoil.org/ideas/bidirectional-type-slicing) (idea, 2025-10-01)

---
Canonical: https://anil.recoil.org/papers/2026-bidirectional-type-slicing
Type: paper
Tags: preprint