Abstract: Development tools report what type an expression has, but not why it has that type. This paper develops a theory of type slicing that answers such questions: a programmer selects a term, queries any part of the type information associated with it, and receives a slice of the program—a well-formed partial program with irrelevant sub-terms folded away—that suffices to reproduce the queried type. We formulate type slicing for bidirectional type systems, where synthesis slices explain the ...