Comment by bluGill

Comment by bluGill 3 months ago

9 replies

Type theory comes from math. Numbers in math do in fact have types. Most of the time we ignore it but numbers in math have types. math also has the concept of max number rolling back to zero ogain something anyone who has studied types in math would know. Rounding error is studied in several different math fields.

negative zero isn't in any math I know of. It is only in obsolete computer science though.

ndriscoll 3 months ago

Mathematicians generally work with sets, not types. The first thing you do after defining the reals is agree that the naturals, integers, and rationals are subsets. From a type theory perspective, they are all type ℝ, and, roughly, the naturals satisfy the proposition "n:ℝ is a natural number".

  • bluGill 3 months ago

    Mathematics has a lot of different theories and some small branches have different rules. I've done mod math for example (it was maybe one week of classes) where you don't get an infinite set of possible numbers. It isn't nearly as interesting as far as mathematicians are concerned (for good reason) so it isn't looked at much but those theories exist.

hilux 3 months ago

I am no Terry Tao, but I do have a degree in mathematics. Other than possibly in a class on numerical analysis, I don't remember anything resembling types.

We definitely spent more time discussing different kinds of infinity than we did discussing rounding error!

I can believe that the situation might be different in "applied mathematics" or definitely in "engineering mathematics" - but at least at Berkeley, the latter degree is in the College of Engineering, not under the Math Department at all.

  • bluGill 3 months ago

    There is a lot of math never taught. types in math are mostly a dead end and so rarely taught - particularly since computer science moved to a seperate department. Even before then it was mostly applied math.

anon291 3 months ago

Contemporary mathematics is duck typed.

  • bluGill 3 months ago

    Usually but when it matters (which is rare) the can use types.

    • anon291 3 months ago

      So, what was the purpose of the conversation then? In the vast majority of cases, in most normal mathematical manuscripts, '3.0' is '3'. There is no distinction.

      • bluGill 3 months ago

        The point is to refute the claim that math never uses a bunch of computer concepts like types - those concepts all have roots in formal math theories and so the claim is false. That that theory is not of much use in the vast majority of math doesn't mean there is no math behind it.

        • anon291 3 months ago

          You said:

          > The right answer they were looking for was 3, not 3.0. Adding that .0 implies a precision which is not correct.

          In contemporary mathematics, 3 is 3.0 . Both 3 and 3.0 belong to the set of integers. There is no additional precision being demonstrated by adding a 0 at the end of the 3. This is simple notation, not refering to a new concept.