[takeoutweight]

Types give you the power of abstraction -- they allow you to define new concepts that "don't to go wrong" and allow you to speak of things other than just bytes-shuttled-on-a-turing-tape. Rigorously justifying the ignorance of the underlying bytes (i.e. being parametric over representation) is an advantage, not a downside.

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...

[dkarapetyan]

If you're doing mathematics then multiplication is the thing you care about and not its representation in any given number/notation system but if you're actually implementing multiplication then you definitely care about the actual bits and bytes. What structure you impose on top of the implementation to make it easier is all nice and well but don't fool yourself into thinking that types are the end of it. In fact to truly impose some kind of type structure so you could reason about what was going on at the hardware level you'd need more than just the integer type or the floating point type because those types don't let you reason about overflow/underflow at such a high level. Any correct implementation would need to worry about those restrictions and consequently would have to represent those restrictions in the type system.

[pinealservo]

It's entirely possible to do so; there are even typed assembly languages and "bitdata" types and typed memory regions.

Types in general can be far more expressive than most people know. Very expressive types are not necessarily easy to work with, though.