I wrote these down ostensibly to prepare for the big it's-almost-the-end-of-the-semester class discussion tomorrow, but I'm also kind of hoping that some of them will come up during the internship interview I have after class. The assignment called for three, but I ended up with four.1
Type recovery as type inferenceThe first sentence of Guha et al.'s "Relationally-parametric polymorphic contracts" begins "Because most dynamic languages lack static type systems ..." This struck me as strange at first glance -- "most" lack static type systems? Isn't the lack of a static type system the defining characteristic of a dynamic language? -- but it's possible that the authors were including gradually-typed languages under the "dynamic languages" heading. On the other hand, the authors might have been considering the type recovery mechanisms used in some dynamic-language compilers (for instance, in Chez Scheme) to be a kind of static type system. Thinking along those lines reminded me of a point that was raised in Meijer and Drayton's "End of the Cold War" paper, but barely mentioned in papers that we've read since then, which is that dynamic languages can and should have a degree of compile-time type inference. Do formal specifications exist of the type recovery systems actually used in compilers? What's the relationship between such systems and the soft typing that Cartwright and Fagan describe?
Logical types for actually untyped languagesTobin-Hochstadt and Felleisen's "occurrence typing" system raises interesting possibilities for static, decidable type checking in untyped languages, but (despite the title of the paper!) the actual implementation of occurrence typing that they describe in "Logical types for untyped languages" has been implemented as part of Typed Racket, which requires type annotations (it's not even gradually typed). As a next step, how about implementing occurrence typing for an untyped or gradually typed language? Would such a system be feasible and practical, or is there too little static type information to be gleaned from most untyped programs for the type checker to have any purchase on them?
What good is blame tracking, really?2
We've considered various papers that deal with contracts and blame. Although the blame tracking systems we've seen so far can tell us which module of a program is at fault for a run-time contract violation, it's not necessarily the case that the particular module that is blamed is actually the one that the programmer will want to change. In practice, errors arise because of complex interactions between modules, and there are infinitely many ways to modify a program to remove a run-time contract violation, only some of which involve changing the module that is raising blame. For instance, a change to some other module might prevent execution from ever reaching the point at which the original module raised blame. Of course, the blame tracking system can't know the programmer's intentions, but one can imagine a blame tracking system that can suggest several possibilities for the provenance of an error. (Such a system could even ask the programmer for feedback and therefore learn over time what kinds of errors are likely and order the suggestions accordingly.)
Bonus extra topic!: Naiveté
In Wadler and Findler's "Well-typed programs can't be blamed", and again in Siek and Wadler's "Threesomes, with and without blame"3, we saw that "naive" subtyping, in which the typing rule for functions is covariant instead of contravariant in the domain, actually turns out to be useful for reasoning about blame and contracts. My follow-up question is: what other "naive" ideas have we overlooked thus far that could be useful for reasoning about and modeling the behavior of contract systems and type systems? To pick a stock example, does naive (non-capture-avoiding) substitution correspond to anything interesting?
- Apparently I do not have decidable static array bounds checking. Yet.
- Cribbed from a comment I left in Chris chrisamaphone's journal recently, in a discussion about whether HCI and PL research have anything to do with each other: A few weeks ago I was telling a friend about some of the recent work being done on blame. He listened to me for a while, then said, "So, the point of this is to have better error messages?" I bristled and was about to say, "No, no, no! It's much more profound than that!" -- but then I realized that "having good error messages" is a profound goal, and that it would be absurd for me to claim that my reason for caring about contracts and blame -- essentially, because I think the math is fun -- is more profound. Blame tracking is interesting in its own right, but it will only help programmers if the suggestions it makes are realistic.
- It is only by a considerable force of will that I'm not making a Coq joke right now.