That seems to describe something rather different from a type system. A type system is something that associates "types" with terms in your language, i.e. expressions have types. That's writing about some system for associating sets (not types) with values, which is a thing that you can do, but it's never going to be an adequate way of doing compile time checks; to get reliable compile time checks you end up having to implement an actual type system, and if you pretend you only have a sets-associated-with-values system then that will go badly.
Hang on, so "integer", "string", and "(function (integer) string)" aren't types? Could you maybe explain what a type is? Because I'm completely lost in this discussion.
> Hang on, so "integer", "string", and "(function (integer) string)" aren't types? Could you maybe explain what a type is? Because I'm completely lost in this discussion.
It's not about what the types themselves are, it's about how they relate to the rest of the program. A type is something associated with terms (roughly, expressions) in a language - you have to have rules for assigning types to every term, or to put it another way you have to exclude terms that you can't type from your language. So saying 2 is of type integer and + is of type integer -> integer -> integer is a start, but for those to be types you need to be able to say that (2 + 2) is of type integer, not just that 4 is of type integer once you've evaluated it.
> A type is something associated with terms (roughly, expressions) in a language
Unless you replace is with can, you're just spewing dogma, not computer science.
Under a particular paradigm, we can choose to associate types with the nodes in the program's abstract syntax tree, and to have types nowhere else. Then within that paradigm, when we say type, we refer to information attached only to the nodes in the program, and nowhere else.
While that is valid, it doesn't speak to everything that type is or can be.
Even, say, the .jpeg suffix on a file is a type, in a certain context.
> Unless you replace is with can, you're just spewing dogma, not computer science.
Words have to mean something if we're to communicate at all.
> Under a particular paradigm, we can choose to associate types with the nodes in the program's abstract syntax tree, and to have types nowhere else. Then within that paradigm, when we say type, we refer to information attached only to the nodes in the program, and nowhere else.
This stuff predates programming, it goes back to formal language research. That's what type means! If you want to mean something else you should say something else.
