arXiv Science⌕ Search

arXiv subjects

Max Carroll

Publications and source records attributed to Max Carroll.

2 recordsLinked to original sources
arXiv2026

Decomposable Type Highlighting for Bidirectional Type and Cast System

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.

cs.PL↗
arXiv2026

Bidirectional Type Slicing

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.

cs.PL↗