Bad ideas in type theory

  • Types as sets and subtypes as subsets.  This may be due to confusing usage in mathematical practice where, for example, we often see references to integers as a subset of reals. But in mathematical usage, people generally understand that while real numbers without fractional parts are a subset of the real numbers, “the integers” usually means “ẗhe algebraic system Z of all integers with the usual binary operations of addition and multiplication. ” (MacLane, Birkhoff). This is why it’s not a surprise that 1/i (for i other than 1) does not have a solution in “the integers” although it has a solution in “the rationals” and “m +x = n” may not have a solution in the natural numbers but does in the integers. Computer scientists keep attempting to reduce this complex relationship between different systems of numbers to subset, but it doesn’t work in math or in computer science. Types are not sets – they are systems. Subtypes, if those make sense at all, are not subsets.
  • Hierarchies. Mathematical types are not organized in a tree structure.  You can start with lambda calculus or primitive recursion on monomials and build out a theory of real numbers or start with the system of reals and limit yourself to Peano Arithmetic or finite arithmetic for that matter. The group Z5 is not a child of the group Z even though you can map Z5 into Z. Relationships between mathematical systems are complex and structural relationships have to be discovered not axiomatized.  Programming Objects in both the general sense and in the sense of object oriented programming are often not organized in tree structures either. Imposing simple schemes on complex relationships only confuses things.
  • Implicit Promotion –  It may be that FORTRAN was the original sinner, promoting “integer” fixed point numbers to floating points in expressions like i*r.  This leads to confusion and they should have required something like (float)i *r  in such expressions.  Implicit promotion is a major weakness in C, for example.