Now you're confusing the implementation with the abstraction. Types can be modeled by tags. They can be modeled by trees. Or any other data structure that you c

Now you're confusing the implementation with the abstraction. Types can be modeled by tags. They can be modeled by trees. Or any other data structure that you can analyze with a program. >The actual function of types, on the other hand, is to prove simple propositions about a program without running it. The value of a tag proves something about the program. You're just proving it at run-time rather than compile time. Which is an artificial distinction anyway, since your static types theorems are being proved during the run-time of your static type checker. All theorems are proven during some run-time.