# Bidirectional type slicing

*2025-10-01 — idea*


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.

## Links

The project was completed as [Max Carroll](https://maxcarroll0.github.io/blog/)'s Part III project, following on from
his earlier Part II work on [gradual type error debugging](https://anil.recoil.org/ideas/gradual-type-error-debugging). The metatheory is
mechanised in Agda, and a linear-time approximation of type slicing is
implemented for the [Hazel](https://hazel.org) programming environment.

The writeup is available as a [preprint on arXiv](http://arxiv.org/abs/2607.12197)
or [here](https://anil.recoil.org/papers/2026-bidirectional-type-slicing).
Status: Completed
Level: MPhil
Year: 2025
Project: Planetary Computing
Supervisors: Anil Madhavapeddy, Cyrus Omar
Students: Max Carroll

## Related

- [.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/papers/2026-bidirectional-type-slicing) (paper, 2026-07-01)
- [Gradually debugging type errors](https://anil.recoil.org/ideas/gradual-type-error-debugging) (idea, 2024-09-01)

---
Canonical: https://anil.recoil.org/ideas/bidirectional-type-slicing
Type: idea
Tags: functional, hazel, types