Types of Types

Several types of types in programming languages by Simone Martini. pdf

We conflate the concept of “type” in programming with the concept of the same name in mathematical logic—an identification which may be good for today but which is the result of a slow convergence of two different paths that started quite apart with different aims.

This slow mutual recognition of the two fields tells a lot on their essential differences. For most of the “types-as-a-foundation-of-mathematics” authors, types where never supposed to be actually used by the working mathematician. It was sufficient that in principle most of the mathematics could be done in typed languages, so that paradoxes could be avoided.

Types in programming languages, on the contrary, while being restrictive in the same sense, are used everyday by the working computer programmer. And hence, from the very beginning in Algol, computer science had to face the problem to make types more “expressive”, and “flexible”.

While mathematical logic types are perceived as constraints, types in programming languages are experienced as an enabling feature, allowing simpler writing of programs, and better verification of their correctness.

While types are pervasive in federated wiki's json, they exist as only a hint as to how an associated structure might be interpreted by software distributed by various and possibly unreliable means. Contrast this with both uses above where the type system is assumed constant and more primitive.

Wiki still resists types as used in literature and more frequently in html where a passage can be declared as an "abstract" or a "quotation" as a means of defending variation in writing style and purpose.