Marshall <[EMAIL PROTECTED]> wrote: > Chris Smith wrote: > > Going back to my > > handy copy of Pierce's book again, he claims that range checking is a > > solved problem in theory, and the only remaining work is in how to > > integrate it into a program without prohibitive amounts of type > > annotation. > > This is in TAPL? Or ATTPL? Can you cite it a bit more specifically? > I want to reread that.
It's TAPL. On further review, I may have done more interpretation than I remembered. In particular, the discussion is limited to array bounds checking, though I don't see a fundamental reason why it wouldn't extend to other kinds of range checking against constant ranges as we've been discussing here. Relevant sections are: Page 7 footnote: Mentions other challenges such as tractability that seem more fundamental, but those are treated as trading off against complexity of annotations; in other words, if we didn't require so many annotations, then it might become computationally intractable. The next reference better regarding tractability. Section 30.5, pp. 460 - 465: Gives a specific example of a language (theoretical) developed to use limited dependent types to eliminate array bounds checking. There's a specific mention there that it can be made tractable because the specific case of dependent types needed for bounds checking happens to have efficient algorithms, although dependent types are intractable in the general case. I'm afraid that's all I've got. I also have come across a real-life (though not general purpose) languages that does bounds checking elimination via these techniques... but I can't find them now for the life of me. I'll post if I remember what it is, soon. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list