Log in

No account? Create an account
Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Integrating static and dynamic typing: some open problems and future research directions [Nov. 22nd, 2010|12:26 am]
Lindsey Kuper
[Tags|, ]

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 inference

The 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 languages

Tobin-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?

  1. Apparently I do not have decidable static array bounds checking. Yet.
  2. 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.
  3. It is only by a considerable force of will that I'm not making a Coq joke right now.

From: neelk
2010-11-22 09:43 am (UTC)
To pick a stock example, does naive (non-capture-avoiding) substitution correspond to anything interesting?

Blum and Ong have a paper, The Safe Lambda Calculus, in which they define a type system for the LC such that only terms safe for non-capture-avoiding substitution are allowed. To understand the loss of expressiveness, recall that Schwichtenberg showed the STLC can represent only the extended polynomials (ie, polynomials + conditionals) as functions over the type of the Church naturals. In the safe lambda calculus, only plain old polynomials are similarly representable.

As a second example, ordinary interpreters (which don't reduce under lambdas) can (and usually are) inmplemented with non-capture-avoiding substitution, since closed values have nothing to capture. IIRC, Benjamin Pierce exploits this fact to simplify his Coq-based PL course, by giving the simple/bad definition of substitution and only ever proving theorems that involve substituting closed values.

I don't know if the "bad cases" of non-capture-avoiding substitution correspond to anything interesting. Maybe something related to state..? I would look at Berry and Curien's old work on concrete data structures and sequential algorithms for ideas, since they implement higher-order behavior via token passing.
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-11-22 04:28 pm (UTC)
To understand the loss of expressiveness, recall that Schwichtenberg showed the STLC can represent only the extended polynomials (ie, polynomials + conditionals) as functions over the type of the Church naturals. In the safe lambda calculus, only plain old polynomials are similarly representable.

Oh, that's really interesting! It's weird to think about that, because if someone were going to go to all the trouble of statically excluding unsafe terms, then, y'know, why wouldn't they just actually implement capture-avoiding substitution? (But oh, wait, is that exactly what -Wshadow does?)
(Reply) (Parent) (Thread)
From: neelk
2010-11-23 09:19 am (UTC)
I don't pretend to fully understand what they're doing, but in the last few years it seems like there's been a big movement of people doing high-powered game-semantic models of linear logic into model checking. So my suspicion is that they are interested in cases where the substitution algorithm is simple in order to make hardware synthesis from lambda terms easier..!
(Reply) (Parent) (Thread)
[User Picture]From: tristmasjedi
2010-11-24 04:58 am (UTC)
I am interested to talk to you about blame assignment sometime -- it is a topic we dabblers in metareasoning take great, if somewhat undirected, interest in!
(Reply) (Thread)
From: (Anonymous)
2011-02-16 03:41 am (UTC)
This article was extremely interesting, especially since I was searching for thoughts on this subject last Thursday.
(Reply) (Thread)
From: (Anonymous)
2011-03-21 04:05 am (UTC)
Hey all, I do really enjoy the actual internet-site!! This is certainly a fabulous page. All of us look forward to reading even more interesting information in which you’ll turn out to be publishing in the future. I have learned a whole lot by this. Thanks for your insight.
(Reply) (Thread)