by David Binder, Ingo Skupin, David Läwen, and Klaus Os­ter­mann

In Pro­ceed­ings of the In­ter­na­tional Work­shop on Type-Dri­ven De­vel­op­ment. ACM Press, 2022.

Ab­stract

Sta­tic types are a great form of light­weight sta­tic analy­sis. But some­times a type like List is too coarse; we would also like to work with its re­fine­ments like non-empty lists, or lists con­tain­ing ex­actly 42 el­e­ments. De­pen­dent types allow for this, but they im­pose a heavy proof bur­den on the pro­gram­mer. We want the check­ing and in­fer­ence of re­fine­ments to be fully au­to­matic. Ex­ist­ing ap­proaches to re­fine­ment types sup­port ex­ten­sive au­toma­tion, but they make var­i­ous trade-offs. In the orig­i­nal sys­tem of Free­man and Pfen­ning, the pro­gram­mer was re­quired to man­u­ally spec­ify all re­fine­ments they want to use. We only re­quire the user to spec­ify the orig­i­nal data type, but not its re­fine­ments, which are dis­cov­ered au­to­mat­i­cally. With liq­uid re­fine­ment types, an ex­ter­nal solver is used to solve the proof oblig­a­tions for the pro­gram­mer. We only use fa­mil­iar tech­niques from con­straint-based type in­fer­ence. The sys­tem of Jones and Ram­say is very sim­i­lar in spirit to our sys­tem, but the re­fine­ments they allow are less ex­pres­sive. They sup­port re­fine­ments which can be ex­pressed as the re­moval of a con­struc­tor from the de­f­i­n­i­tion of a type, but re­quire this re­moval to be hered­i­tary. So they can­not ex­press the type of non-empty lists which re­quire the re­moval of the Nil con­struc­tor only at the toplevel. We sup­port all re­fine­ments that can be ex­pressed as a reg­u­lar sub­lan­guage of the orig­i­nal type. In this ar­ti­cle we pre­sent a sim­ple re­fine­ment type sys­tem and in­fer­ence al­go­rithm which uses only vari­ants of fa­mil­iar con­cepts from con­straint-based type in­fer­ence. Con­cretely, we build on the al­ge­braic sub­typ­ing ap­proach and ex­tend it with typ­ing rules which com­bine prop­er­ties of nom­i­nal and struc­tural type sys­tems in a novel way. De­spite the sim­plic­ity of the ap­proach, the re­sult­ing type sys­tem is very ex­pres­sive and al­lows to spec­ify and infer non-triv­ial prop­er­ties of pro­grams.