But maybe I am misunderstanding your comment? Perhaps you were just equivocating over what "really there" means? If that's the case, is multiplication not "really there" because it can be implemented in terms of bit shifting and addition? We don't imagine multiplication as somehow putting these restrictions on what we can do with our bit shift operators -- the multiplication is the "real" thing we care about and the binary operations are incidental.
In any case, see the famous parable that opens Reynolds' "Types, Abstraction, and Parametric Polymorphism" for a colourful example of ignoring the underlying data representation:
http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types...
Types in general can be far more expressive than most people know. Very expressive types are not necessarily easy to work with, though.
Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things.
edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
What you can bet is that absolutely no-one is excited about mission-critical software failing because of a bug that could have been caught by testing... or type checking.
If you scanned through a program looking for syntactic forms that represent types as such, you could find clear examples of such syntax in most programs; some programs would have more and some less, probably determined to a large extent by programming language. It would be things like variable declarations, class declarations, etc. -- essentially declarative scaffolding, which wraps and adds meaning and context to code that does things; the type code itself, though, generates no cpu instructions, because its purpose isn't to represent action, it's orthogonal to action.
You could argue that type code causes actions to be performed, such as when types need to be casted, which may trigger some kind of transformation on the underlying data. But, even though the type helps trigger action (the data transformation), the type is not that action.
I don't know if what I've written will make sense or sound like empty nonsense... but the article itself makes the point that you will generally not find types in machine code; at most you can find indirect evidence that they were there.
You may say, "what difference does that make? Why make the distinction?"
Well, machine instructions are what make the computer do observable things. Any code you have to write that doesn't produce instructions needs to be justified somehow. There are lots of ways of justifying such extra code. But it's orthogonal to actually doing things -- pretty much by definition.
Edit -- to respond more directly: >>What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable).
I think that's a real risk. People tend to get attached to ideas about programming languages in quasi-religious fashion; I think it's healthy to stay in touch with an objective cost/benefit perspective, though. The user doesn't see the code, he/she only sees the results. And the experience of the user is what you should focus on as a programmer -- right?
>>Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things.
I'm not sure I follow the distinction you're making, between the textual representation of the code and -- what? Clearly the text has to be written before the computer will do anything -- so it must be important.
>>edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
I said types don't do anything, and that they don't excite me. I didn't say we should get rid of all types. Tests don't do anything, either (at least, they don't do what the program should do). Tests also don't excite me. That doesn't mean that testing is pointless. Testing can be costly and tedious -- but you have to weigh that against the risk of bugs getting through.
> Well, machine instructions are what make the computer do observable things.
The typechecker is a program, and if the typechecker fails, you will see output.
Typecheckers definitely do things. But are those things interesting?
That seems like asking "seat belts definitely do things, but are those things interesting?"
So, thanks for the well wishes, but in this case I don't think they're needed: any reasonable compiler should be able to do this without great difficulty.