It is really unfortunate that people down vote something that is wrong without actually saying what is wrong about it. I think it would help, though, to acknowledge that your opinion is unlikely to be shared with others and to append something like, "Can anyone explain where I'm going wrong?"
Now, I don't actually know much about type theory at all and came here to try to remove some of my ignorance. As such, I can't really help you much, but I will try my best. You might want to look at: https://en.wikipedia.org/wiki/Type_theory
If I read it correctly (and if it is written correctly), a "term" is essentially anything with a "type". So 1, 2 and 3 are terms and they have a type. A "function" is something that takes terms and "reduces" them to other terms. You can "apply" a function to some arguments in order to reduce them. So if we have a function, "myfunc x", we can apply that to 2 and have "myfunc 2". Both "myfunc x" and "myfunc 2" are terms, but they have different types.
Let's make a function that doubles an integer (let's call the type "int"). So "double x" is a term with a type of "int -> int": it maps an int onto an int. "double 2" is a term with a type of int. The term "double double 1" can be "reduced" to the term "double 2". "double 2" can be "reduced" to the term "4". 4 is known as a "normalized term". It can not be reduced any further.
Now, you may be saying "How is this different from what I said?" From what I can tell, the main difference is that a type is not a set of "values" (or normalized terms). Functions applied to terms also have a type. Functions with free variables also have a type. Anything that is a term in an expression has a type. So 1, 2 and 4 are of type int. "double 1", "double 2", and "double double 1" are also all of type int. If we had a function called "fortytwo" that just returned 42, it would also be of type int.
It may seem like a small (possibly insignificant) difference, but it really depends on your point of view. We can completely ignore the type if we want to. Many programming languages make that very easy. We could also subscribe to the idea that a type is just a set of values, like you said. We can write many fine (and many not-so-fine) programs with that point of view.
These views limit the kind of analysis we can do on the code that is written, though. The point of using type theory in computer languages is to help us reason about the code analytically. So my answer to your (unasked) question is, it doesn't have to be complicated. It proves useful to include all of the nuances that type theory gives us. Intentionally putting blinders on to make it seem simple, just deprives us of potentially useful capabilities.
Hopefully someone who actually knows something about this topic will chime in and correct whatever horrible mistakes I've made.
You're right - I am thinking "How is this different from what I said?".
> Functions applied to terms also have a type.
Yes, and those types are sets of values. For example, "int -> int" is the set of all functions that map integers to integers. (Remember that functions are also values, just like any other value, in functional programming.)
Now, I don't actually know much about type theory at all and came here to try to remove some of my ignorance. As such, I can't really help you much, but I will try my best. You might want to look at: https://en.wikipedia.org/wiki/Type_theory
If I read it correctly (and if it is written correctly), a "term" is essentially anything with a "type". So 1, 2 and 3 are terms and they have a type. A "function" is something that takes terms and "reduces" them to other terms. You can "apply" a function to some arguments in order to reduce them. So if we have a function, "myfunc x", we can apply that to 2 and have "myfunc 2". Both "myfunc x" and "myfunc 2" are terms, but they have different types.
Let's make a function that doubles an integer (let's call the type "int"). So "double x" is a term with a type of "int -> int": it maps an int onto an int. "double 2" is a term with a type of int. The term "double double 1" can be "reduced" to the term "double 2". "double 2" can be "reduced" to the term "4". 4 is known as a "normalized term". It can not be reduced any further.
Now, you may be saying "How is this different from what I said?" From what I can tell, the main difference is that a type is not a set of "values" (or normalized terms). Functions applied to terms also have a type. Functions with free variables also have a type. Anything that is a term in an expression has a type. So 1, 2 and 4 are of type int. "double 1", "double 2", and "double double 1" are also all of type int. If we had a function called "fortytwo" that just returned 42, it would also be of type int.
It may seem like a small (possibly insignificant) difference, but it really depends on your point of view. We can completely ignore the type if we want to. Many programming languages make that very easy. We could also subscribe to the idea that a type is just a set of values, like you said. We can write many fine (and many not-so-fine) programs with that point of view.
These views limit the kind of analysis we can do on the code that is written, though. The point of using type theory in computer languages is to help us reason about the code analytically. So my answer to your (unasked) question is, it doesn't have to be complicated. It proves useful to include all of the nuances that type theory gives us. Intentionally putting blinders on to make it seem simple, just deprives us of potentially useful capabilities.
Hopefully someone who actually knows something about this topic will chime in and correct whatever horrible mistakes I've made.