λdB: Blame tracking at higher fidelity

Jakub Zalewski, James McKinna, J. Garrett Morris, Philip Wadler

Research output: Contribution to conferencePaper

Abstract

This paper introduces λdB, a blame calculus with dependent types. It supports dependent functions, predicate refinement at all types, the dynamic type, and full blame tracking. It is inspired by and extends previous work on hybrid types and Sage, by Flanagan and others; manifest contracts, by Greenberg, Pierce, and Weirich; and blame calculus by Wadler and Findler. While previous work only allows refinement over base types, λdB supports refinement over any type. We introduce novel techniques in order to prove blame safety for this language, including a careful analysis that reduces open judgments on terms to closed ones on values, and the idea of ‘subtyping with a witness’, which fix flaws in the previous work of Wadler and Findler. These technical contributions mean that we can achieve a completely operational account of the metatheory of our language, and thereby avoid the need to intertwine operational and semantic models which bedevils the work on hybrid types and manifest contracts.
Original languageEnglish
Publication statusPublished - 2020
EventFirst ACM SIGPLAN Workshop on Gradual Typing 2020 - New Orleans, United States
Duration: 19 Jan 202025 Jan 2020

Conference

ConferenceFirst ACM SIGPLAN Workshop on Gradual Typing 2020
Abbreviated titleWGT 2020
CountryUnited States
CityNew Orleans
Period19/01/2025/01/20

Fingerprint Dive into the research topics of 'λdB: Blame tracking at higher fidelity'. Together they form a unique fingerprint.

  • Cite this

    Zalewski, J., McKinna, J., Morris, J. G., & Wadler, P. (2020). λdB: Blame tracking at higher fidelity. Paper presented at First ACM SIGPLAN Workshop on Gradual Typing 2020, New Orleans, United States. https://wgt20.irif.fr/wgt20-final98-acmpaginated.pdf