Types define the encoding for some pure mathematical thing, and they define the set of things that can be done to objects in that encoding. Something is the sam

Types define the encoding for some pure mathematical thing, and they define the set of things that can be done to objects in that encoding. Something is the same type as something else iff they share representation and a particular set of operations. There are ideal types, and there are practical types. UTF-8 and Unicode are great examples of a practical type. Null-terminated UTF-8 is a type, but unicode is an alphabet of characters in the abstract. The type called "UTF-8 string" has certain permitted operations, and a particular representation in machines. Another good example is the set of all integers modulo 2^x, and the type consisting of unsigned x-bit binary integers for x86-style processors. The x86 add operation is permitted only on the later, which makes it a distinct type from, say, the PPC integer type. (so does endianness, but that's encoding, not the op) Ideal types are things like sets, trees, lists, and so on. Their encoding is such that all everything is possible. Look at any functional language. These things are in math, although often less formally defined. The only problem with ideal types is that bottom is a member, which is a problem for some operations permitted on said ideal type. To put this all another way, types convey something terribly important: What is this thing, and what operations can I do with it. In math, we tend to hand-wave both of these things away, and instead rely on human intuition to determine what something is (set, integer, field, vector, etc.) and what we can do with it (intersect, add, integrate, rotate, etc.) But if you look hard, you'll see types in math. Vectors are bold, fields have arrows, integers have an initial assignment, sets are capital letters, and so on. A human must do type analysis to figure out of an operation or encoding is conforming.