# Decomposable Type Highlighting for Bidirectional Type and Cast System

*2025-01-01 — paper*

Authors: Max Carroll, Anil Madhavapeddy, Patrick Ferris


We explore how to provide programmers with an interactive interface for
explaining the process by which static types and dynamic casts are derived,
with the goal of improving the debugging of static and dynamic type errors. To
this end, we define mathematical foundations for a decomposable highlighting
system within a bidirectional system and show how these can be propagated
through dynamic types in a cast system. Our prototype implementation in the
gradually typed Hazel language includes a web-based user interface, through
which we highlight the importance of type-level debugging.

This was [presented at HATRA 2025](https://anil.recoil.org/notes/icfp25-what-i-learnt) colocated with ICFP 2025.


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

## Related

- [.plan-26-29: Perfect weather, imperfectly measured, precisely predicted](https://anil.recoil.org/notes/2026w29) (note, 2026-07-19)
- [What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP](https://anil.recoil.org/notes/icfp25-what-i-learnt) (note, 2025-10-09)

---
Canonical: https://anil.recoil.org/papers/2025-decomposable-type-highlighting
Type: paper
Tags: preprint