My Thesis

Heuris­tic com­piler diag­nos­tics can­not always local­ize type class errors; inter­ac­tive visu­al­iza­tion of type class res­o­lu­tion is fea­si­ble and with few inter­ac­tions facil­i­tates local­iza­tion.

Pro­gram­mers crave abstrac­tion. Through­out the his­tory of com­put­ing researchers and engi­neers have sought to manip­u­late data via higher-level abstrac­tions. One such abstrac­tion is poly­mor­phism, the abil­ity for a sin­gle sym­bol to rep­re­sent a set of types. There are sev­eral fla­vors of poly­mor­phism. Para­met­ric poly­mor­phism, a func­tion para­me­ter­ized by a type, which includes Java generic func­tions or C++ tem­plates. Sub­type poly­mor­phism, oper­a­tions can act over a set of types given they’re related by a notion of sub­sti­tu­tat­bil­ity, a fancy way of say­ing object-ori­ented sub­typ­ing. Lastly, ad-hoc poly­mor­phism, a set of func­tions and types that may have mul­ti­ple con­crete imple­men­ta­tions, and the focus of this the­sis.

Impor­tant Note The tool pre­sented in this the­sis, Argus, is open-source,https://github.com/cog­ni­tive-engi­neer­ing-lab/argus and avail­able as a VSCode exten­sion on both the VSCode Mar­ket­place and Open VSX Reg­istry.

Overview

This dis­ser­ta­tion has the fol­low­ing struc­ture:

  • The rest of this chap­ter intro­duces type classes as a lan­guage abstrac­tion, impor­tant ter­mi­nol­ogy for dis­cussing the lan­guage of type classes, and a basic exam­ple.
  • The fol­low­ing, , intro­duces the struc­ture of error diag­nos­tics in Rust. Most impor­tant is our cri­te­ria for what dis­tin­guishes good and poor class diag­nos­tics. The chap­ter fin­ishes by demon­strat­ing the con­nec­tion between logic pro­gram­ming and type class sys­tems, then pro­pos­ing our solu­tion to local­ize trait errors in Rust.
  • After estab­lish­ing the foun­da­tion for why inter­ac­tive debug­ging ben­e­fits type class sys­tems, we talk about the imple­men­ta­tion of our novel tool, Argus, that pro­vides an inter­ac­tive debug­ging inter­face into Rust’s trait sys­tem. We dis­cuss the chal­lenges and archi­tec­ture of the tool as well as future plans for improve­ment. The chap­ter fin­ishes by pre­sent­ing our eval­u­a­tion of the tool on a com­mu­nity curated test suite of hard-to-debug trait errors.
  • We close with an infor­mal look at the broader research area around inter­ac­tive debug­ging, type error local­iza­tion, and proof tree debug­ging.