What To Know Before Debating About Type Systems
I started writing this as a blog entry, but it reached 15 pages. So it moved to a place of its own.
I’ve tried to be reasonably fair. Enjoy!
I started writing this as a blog entry, but it reached 15 pages. So it moved to a place of its own.
I’ve tried to be reasonably fair. Enjoy!
Sententia cdsmithus 
That looked like it could be very interesting. Sadly the link is broken, could you please put your document online again ?
—
Jedaï
The document is still there, and the link works from where I am. Perhaps the system was just temporarily down or there was a router issue? Let me know if you can try again and reach it.
Forbidden
You don’t have permission to access /types.html on this server.
Thanks for pointing that out. My web host somehow managed to go in and screw up all the permissions on files! Fixed now.
Well, the page is gone. Please publish it again. It is linked to from many places.
Thanks!
http://www.twu.net could not be found :(
Could you please publish it again?
http://www.pphsg.org/cdsmith/types.html
Chris,
The link seems to be dead at the moment (the domain appears to have expired).
I would be very grateful indeed if you could ensure that it remains available (at its original location or elsewhere). It’s comfortably the best framing of the debate that I’ve seen, and I would greatly miss it (as, I suspect, would many others).
Thanks in advance!
Paul.
This article, which I agree is excellent in its content, is apparently very unstable on the internet. It’s currently 404ing at twu.net (although twu.net itself is apparently up), and the entire pphsg.org site is down.
Chris Smith, your adoring fans wish you’d put your damn excellent article in a more reliable place! :P We want to tell people to STFU and RTFM, and then link to you!
For those reaching this page, here’s one way to read the article:
http://web.archive.org/web/20080822101209/http://www.pphsg.org/cdsmith/types.html
You really should stick with the practical stuff, because you get all the theoretical stuff wrong. For instance, Rice’s Theorem doesn’t say that you can’t check a program for correctness, it says that no single algorithm can infallibly determine the correctness of *every* program; but many specific programs can be proven correct or incorrect. And of course there *are* type checkers that don’t reject any correct programs — unless you have a bizarre notion of correctness by which syntactically invalid programs are deemed “correct”. Even then, if all operations on all types are defined, the type checker will have no opportunity to reject the program. For example, consider a system in which any value is implicitly converted to its string representation if no other operation applies — i.e., if otherwise the type checker would reject the program. There’s no “ironclad mathematical proof” that “it’s impossible” to build such a system; it’s readily realizable.
Ignoring the insulting tone, I’ll answer what you said.
If I understand what you’re saying about Rice’s Theorem, then you are correct. This seems to be a question of definitions, and I’m reading the original text that I wrote several years ago and having a hard time seeing how it could be misinterpreted in that way. After all, I did say “There will be some programs for which the answer is easy; … However, there will be some complicated programs for which my program can never figure out the answer.” I then went on to write in great detail about approximations that give bounds on the answer but never quite completely determine the answer. So we seem to have no actual disagreement here.
As for the latter part, it is a fact that no type checker can determine any non-trivial proposition about the output (or visible behavior) of a program. Okay, I’m guessing that somewhere perhaps I forgot to repeat the “non-trivial” condition, since your counterexample is to point out the trivial type checker that rejects no programs at all. If this actually, confused you, let me apologize and assure you that you’re right, you can indeed write a type checker that always accepts (or always rejects) a program regardless of its content. Outside of those two cases, what I said is true.
If you’re thinking of syntax checking, that’s changing the question. Syntax isn’t a question of the behavior of the program; it’s a question of whether you’ve got a program at all. You’d have a hard time convincing many people that a piece of text that gives syntax errors if you try to compile it is reasonably described as a program.
The links to this article (except for the Wayback machine archive) are long since dead. It’s a good article–could you submit it to a journal so it can then be cited properly? Preferably one that is hosted online, of course.
If it helps, I’ll grab the text and re-post it as a blog entry here, where it’s likely to be available for longer. As for a journal, umm, it’s pretty far away from journal-quality work. It’s just a light commentary on some very general ideas. I do mathematics research and publish in journals for a living, and trust me, there’s a huge chasm between the two.
I think it would be fine for a publication like The Monad Reader. Maybe you could send it there.