• http://davidpisarra.com/inspirational-guesting-on-lisa-mcdonalds-carpe-diem-show/feed 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 integers are a subset of the real numbers, “the integers” usually means “the 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/n for  (|n| > 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.
  • Aurogra no prescription 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 the elements of 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, automatically  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.

 

Bad ideas in type theory
Tagged on: