What is a type error?

[Chris Smith]

Marshall <marshall.spight at gmail.com> 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