Where do types come from?

Some mathematicians are trying to formulate a basis for mathematics in type theory. For example, there is the Univalent Foundations of mathematics proposed by Vladimir Veovodsky. This reduces logic, set theory, category theory (actually groupoids) and higher abstractions to homotopy theory (well, certain explicit constructions in such anyway) which is then modelled in Martin-Löf type theory.

By the Curry-Howard isomorphism there is a correspondence between types and proofs (specifically types in the simply typed lambda calculus and proofs in the intuitionistic logic or if you add dependent types, then also predicate logic).

The real difference is that functions in type theory are computable, whereas functions in mathematics (based on sets) need not be.

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.

A real discussion about Frege, Russel, Curry, etc and how that lead to what programmers use today would have been truly interesting.

eg. When multiplying integers and matrices respectively you'd use a different algorithm to compute the result of multiplying the respective types.

Types mostly disappear as well when using a language derived from the lambda calculus vs. the universal turing machine.

:(