← Back to context

Comment by jiggawatts

1 year ago

Mathematics is surprisingly weakly typed.

For example, the "2" in "2π" is not the same type of "2" as in x^2 or 2x generally. Yet, physicists (to pick a random group) will blend in these factors, resulting in nonsense. As a random example, one of the Einstein field equations has "8π" in it. Eight what!? What aspect of the universe is this counting out eight of -- a weirdly large integer constant? This actually ought to be "4(2pi)", and then "4" is the number of spacetime dimensions, which makes a lot more sense.

Similarly, in at least one place the square of the pseudoscalar (I^2) was treated as a plain -1 integer constant and accidentally "folded" into other unrelated integer constants. This causes issues when moving from 2D to 3D to 4D.

These examples miss the mark somewhat. The "2" in "2π" can mean several things (the nonnegative integer 2, the integer 2, the rational 2, the real 2) that are all commonly identified but are different. The "2" in "x^2" usually means the nonnegative integer 2. The "2" in "2x" can usually mean the nonnegative integer or the integer 2, but also the other 2's depending on what x is. The problem is not that the meaning of 2 varies across different expressions, but that it can vary within each single expression.

The best example is perhaps the polynomial ring R[x][y], which consists of polynomials in the variable y over the ring of polynomials in the variable x over the real numbers. Any algebraist would tell you that it is obviously just the two-variable polynomial ring R[x, y] in disguise, because you can factor out all the y-powers and then the coefficients will be polynomials in x. But the rings are very much not the same at the level of implementation, and every time you use their "equality" (canonical isomorphy), you need to keep the actual conversion map (the isomorphism) in the back of your mind.

Haskell shows (one way of) how you can have numerical literals like 2 that can be used with many different types, but still be strongly statically typed.

That by itself isn't a problem. But making all the other confusions you mention is a problem.