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

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.)