3 ms·

I didn't say that types are tags at a different time, I said they are different things. And only concrete types are about representation. Abstract, universal,

• kazinator 12y ago
  But a concrete value, like a symbol or string, has a concrete type, and that better agree with what its tag information says (if it has it). Sure, expressions like "for all x: function from x to x" may not have concrete instantiations: there is no thing that is type tagged that way. It could be, of course; there is no limitation on what constitutes a type tag. Any compile time information, whether it is a universally quantified expression or whatever, can be represented at run-time also. In practice, that isn't done.