10 ms·

Is Mathematics, as a language, considered typed in general?

• adamnemecek 9y ago
  Most mathematics isn't constructive (https://en.m.wikipedia.org/wiki/Constructivism_(mathematics) https://en.m.wikipedia.org/wiki/Constructivism_(mathematics)) so it doesn't really come up I think. E.g. you know how matrices need to have a certain shape to be multiplied? People don't really talk about what happens if they don't. Physics on the other hand very much has types, the unit to type correspondence is dopetastic.
  • kruhft 9y ago
    But what about Russel's type system(s)? Were they just an addition he proposed that never went anywhere, or are they used much like certain programming languages have types and others don't, depending upon the preference of the user? Or are types just 'too hard/restricting' for general mathematics?
    • danharaj 9y ago
      Russel and Whitehead's type system never gained significant traction. It's primarily of historical interest. Once mathematicians became convinced that ZF set theory over first order logic was plausibly consistent and expressive enough, such foundational issues became less important to the typical mathematician. Lately there's been a resurgence in foundations because of what new foundations like Homotopy Type Theory bring to the table. Funny how something as basic as equality can be revisited time and time again for thousands of years!
      • pmoriarty 9y ago
        "Once mathematicians became convinced that ZF set theory over first order logic was plausibly consistent and expressive enough, such foundational issues became less important to the typical mathematician." Was this decision ever explicitly expressed and agreed on by mathematicians at the time, or was it just implicitly adopted?
        • danharaj 9y ago
          A bit of both over the years.
  • AnimalMuppet 9y ago
    ELI5: Why would constructive math be more typed than non-constructive math?
    • adamnemecek 9y ago
      Constructive mathematics is based on intuitionistic logic (i.e. classical logic without law of the excluded middle, meaning you don't have proof by contradiction, to demonstrate the existence of something you have to "construct" it). Intuitionistic logic is very close to type theory.
      • AnimalMuppet 9y ago
        OK, ELI10: Why or how is intuitionistic logic very close to type theory? Is it based on type theory? Or is it just similar? In either case, how and why?
        • adamnemecek 9y ago
          Good ol' Curry-Howard isomorphism. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... But the connections don't really end there.
        • rraval 9y ago
          See https://codewords.recurse.com/issues/one/type-systems-and-logic https://codewords.recurse.com/issues/one/type-systems-and-lo... for a pretty elaborate response to this question. tl;dr: types are propositions and values are proofs of those propositions. Constructive logic is not concerned with (true xor false), but rather "I can prove A" or "I can prove not-A". There's also the middle ground of "I don't know how to prove anything about A".
        • Retra 9y ago
          They are models of each other. You can translate statements in one to statements in the other by using some relatively simple rules.
    • 9y ago
  • marcosdumay 9y ago
    Physicists just love to work on natural unities, where they throw their types and conversion functions out of the window and calculate in a unityped framework.
    • adrianratnapala 9y ago
      Checking your units is a basic sanity check that we teach students. But as we advance, physicists throw away that wisdom. Theorists especially have an annoying habit of doing this, because all the repetitions of "c", "hbar" etc "k_B" etc clutter up their equations. But I preffer to keep that stuff in, even when doing pretty abstract stuff. Essentially because I wanted the type annotations. For example my favorite convention for the Minkowski metric is: [c^2 0 0 0] [ 0 -1 0 0] [ 0 0 -1 0] [ 0 0 0 -1] That way your vectors are just $(t, x, y, z)$, where $t$ has units of time and the rest of space. Your covectors do come out oddly as $(c^2t, -x, -y, -z)$, but that's what makes them covectors.
      • catnaroek 9y ago
        Alternatively, you can work with x^0 = ct instead of x^0 = t.
        • adrianratnapala 9y ago
          Yes, and and that a much more common convention than the one I favour. They do it partly because it keeps the factors of c out of the visible equations -- but I like my those cs. Another reason is that people instinctively feel that the elements of the coordinate tuple all have to have the same units. But that's not necessary when you have a metric around. Indeed keeping irregular units is helpful because it prevents you from accidentally forgetting to multiply through by the metric.
          • catnaroek 9y ago
            The c factor doesn't really go away. It just gets shifted into 4-vectors.
• heinrichhartman 9y ago
  I don't know my way around Type theory, but I have done a fair bit of Mathematics and Programming. Mathematics is largely based on set theory, so every element has a set it belongs to, and every function has a source-set (domain) and a target-set (co-domain). Mathematicians are very careful to always qualify the encompassing sets, domains and co-domains. You would always write: * Let x \in X be a point in Space. * Let f:A->B be a fuction with ceratin properties. This is even more pronounced in Category theory, which invaded algebra and geometry quite heavily. Where the only thing you know about a function is it's domain, codomain and how it composes. So, yes. Mathematics on a practical level is _very_ type aware. And it also prevents you from doing stupid stuff: f:A->B, g:A->C, can't be composed, so f(g(x)) is a "type error".
  • Drup 9y ago
    While Mathematics is type aware, Mathematicians often aren't. They mix things that are "not the same object, but almost, I swear", and constantly write ill-typed expressions. This is generally on purpose, to avoid making explicit things that are obvious, but as someone developing and using statically typed languages, reading Math papers is often quite frustrating.
• nerdponx 9y ago
  I assume that by "mathematics" you mean" mathematical notation". No, but static type hinting is strongly encouraged. If I say in my paper that "x" is a vector, if I later use "x" to mean a scalar it would cause tremendous cognitive dissonance and confusion for the reader. There is no compiler error, in that the information can still be read and understood. It is just much more difficult. Mathematical notation is also aggressively polymorphic. The expression "f x" can have wildly different meanings depending on what "f" and "x" are.
• gertef 9y ago
  Mathematics is not a language. Your question is like asking if database-backed web applications are typed. Mathematics is often expressed in language, That language us usually a mix of a human natural language English/French/German/etc plus symbolic extensions, and that is very poorly typed. In the recent failed proof of P!=NP, the flaw was a type error: https://cstheory.stackexchange.com/questions/38803/is-norbert-blums-2017-proof-that-p-ne-np-correct/38823 https://cstheory.stackexchange.com/questions/38803/is-norber... Type errors are rather common in math proofs that end up retracted. But it's hard to call them type errors, because it's not like a computer program where the typechecker detected the collision or failed in some way: the proofs make very little mention of types at all, and it's up to the readers to apply a type-system from their own heads.
  • kruhft 9y ago
    The conveyance of mathematics from one mind to another must be done with some form of language.
    • adrianratnapala 9y ago
      This is trivially true, but only because you can keep stretching the definition of language. For example suppose a geometer explains something to another geometer just by drawing diagrams with no verbal or textual annotation. You can plausibly claim that "geometry diagrams" are a language, but now you are defining language so broadly that the term is almost useless.
      • kruhft 9y ago
        Why would you say that "geometry diagrams" are not a language? Google, define language: lan·guage ˈlaNGɡwij/Submit noun 1. the method of human communication, either spoken or written, consisting of the use of words in a structured and conventional way. "a study of the way children learn language" 2. the system of communication used by a particular community or country. "the book was translated into twenty-five languages" synonyms: tongue, mother tongue, native tongue; More I would say "geometry diagrams" are a language, by the second definition.
• tel 9y ago
  Generally, no. As others have mentioned, Mathematics isn't really a language. It's at the very least absolutely certainly not one language. Certain parts of Mathematics use a typed language. Certain parts rely on other kinds of containment properties which serve nicely as types. Finally, generally, math is very interested in being completely clear the properties of objects and very interested in speaking abstractly, so even if the language of use is untyped the logic is often very rigorous around typing. Above it all, perhaps, is the idea that mathematics is concerned with proof and proofs may contain reference to the properties being discussed---metamathematical ideas pervade normal mathematical thought. This means that even absent of types the content of a mathematical utterance is often going to explicitly posit, discuss, and prove properties similar to type propositions.