Technical reports

Polymorphic type slicing

Max Carroll

July 2026, 65 pages

This technical report is based on a dissertation submitted May 2026 by the author for the degree of Master of Engineering (Computer Science Tripos) to the University of Cambridge, Sidney Sussex College.

Abstract

This dissertation formalises and mechanises type slicing – a technique that incrementally explains program types by highlighting minimal program fragments. Using this, a programmer can select any sub-term of a program and incrementally explore complex types and concisely explain type errors. Crucially, this includes highlighting context surrounding the term, differing from typical type error highlighting, which simply states that a term has the wrong type, but not what about the surrounding context explains why it has this type.

This is formalised in a bidirectional, gradually typed core calculus with explicit System F style polymorphism, products, and sum types. A novel context classification judgement formalises the notion of splitting type information into that derived from a selected sub-term and that coming from the surrounding context, and can be applied to arbitrary bidirectional type systems. Further, the theory extends formally to ill-typed programs with error marks, building upon the marked lambda calculus of Zhao et al. Essentially the whole construction is mechanised in Agda.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-1007,
  author =	 {Carroll, Max},
  title = 	 {{Polymorphic type slicing}},
  year = 	 2026,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-1007.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-1007},
  number = 	 {UCAM-CL-TR-1007}
}