[barrkel]

There's types as defined in a spec, and types according to type theory.

In short, I think the spec is incorrect in its use of the concept of types; or incomplete.

You'll note that the spec uses the concept of "internal properties" to distinguish between the different things one can do with values. From a type theory perspective, these internal properties and the implied permitted operations come close to type definitions. It's a matter of perspective, then, when one is using the word 'type' as defined by a particular language's spec, or 'type' as in programming language pragmatics / type theory POV. For the generalist programmer who knows more than one language, a broader concept of types is usually more useful.

Further, the spec uses these internal properties solely to define the semantics of the language, and they are not necessarily visible artifacts of any implementation. Talking about them as if they were concrete confuses the map with the territory.