6 ms·

If by "type systems/checking" one refers to constraints on "valid operations in context" like comparisons, subtractions, additions (or maybe in a prog.lang cont

by cb321 5y ago

If by "type systems/checking" one refers to constraints on "valid operations in context" like comparisons, subtractions, additions (or maybe in a prog.lang context assignment to lexically static identifiers) then physical units of measure (seconds, meters|its ancient cousins, etc.) were the first type system. I.e., one cannot add/compare/etc. meters & seconds without conversion and not all conversions are possible. This remains the first such system most people learn in elementary school. Historically such ideas arose along with measurements themselves and computations upon their results like comparison/subtraction/even taxation. Yes, this is all (typically) manually checked and explicit metadata symbols are carried through calculations. I still think it's the primordial example that few mention in discussions like these.

tel 5y ago
Yeah, saying Russell invented types is fun but horribly wrong. He invented other things and stood at the center of an explosion in formal logics. But types are way old.
- JoBrad 5y ago
  Maybe he invented it the way that many people think the color blue was invented? Causing everyone to see something for the first time (especially when it was right under our noses) is certainly impressive.
  - EarthLaunch 5y ago
    In my game design I've imagined two parallels to invention; discovery and identification. All three are learning about the world, but in slightly different ways. Invention: I created that. Discovery: I found that lying around. Identification: I conceptualized a definition for that.
  - tel 5y ago
    This is certainly more true. That explosion of logics I mentioned was a big movement of many authors to expand our understanding of types (among other things).
- titzer 5y ago
  When people say a mathematician "invented" something, it's understood that they didn't create it from nothing. Newton didn't "invent" gravity, for example, he just came up with the first mathematically rigorous theory for it. Same for Russell and types.
  - wlib 5y ago
    This shows a funny way that the word invent has shifted in meaning. Invent means “found” (almost literally “came upon” in Latin) - yet for some reason it shifted to mean “created” in a sort of “this is mine don’t steal it from me” sense. Then here we are clarifying that we literally mean the actual meaning of the word. It’s interesting that math is considered impossible to have as intellectual property, yet we think somehow that IP law is justifiable for everything else.
    - titzer 5y ago
      Yeah, that is odd. The german word is "erfunden" which is something like "completely found".
    - Koshkin 5y ago
      > we literally mean the actual meaning Also, in the everyday speech the word "literally" no longer means what it was meant to mean.
  - tel 5y ago
    I understand that distinction. Russell came up with a mathematically rigorous theory for the foundations of mathematics and happened to use a very simple type system to accomplish it. He wasn't the first to formally make use of types, though he may have been the first to use that term. He also seriously pushed forward our techniques of mathematical rigor, so in some sense he "invented" many, many, many things. To be clear, I think Russell was an amazing mathematician and inventor. I also think that the history of types is way more rich and interesting than just saying that he invented the idea. To not mention at least Frege is to miss a lot.
Aerroon 5y ago
I had never thought of type systems in this way. If type systems are effectively a "unit" attached to the data then you can think of them as an unknown value in arithmetic. Eg "4x + 4y = 40.4z" x, y, and z here are units: x is meters, y is centimeters, and z is decimeters. You could do the same with types. The computer only knows the binary value, but the type assigns meaning to the value just like physical units do. This must've been really obvious to a lot of people, but it only clicked just now for me. Thank you.
- kroltan 5y ago
  By analogy, that's also how type inference works. If you know X, and either the type-rules for arithmetic, or Z, you can figure out Y. The constraints of their usage can be used to determine the type required of that data.
- 10000truths 5y ago
  I think of it the other way around - dimensional analysis of units is a special case of a type system. Two units of different measures cannot be added/subtracted with one another. Units of the same measure (e.g. length: cm, in) are trivially convertible via a scalar factor (e.g. 2.54 cm/in), and units of different measures (e.g. length: m, time: s) can be multiplied/divided to get a new unit of measure (speed: m/s), although some such units might have no practical use.
  - cb321 5y ago
    Dimensional analysis of units is absolutely a special case (I said "primordial example") of type systems. Proof: "constrained operations" and "notional objects" are very limited/somewhat concrete - "additive/comparative/conversion-y" and "measured things". Modern notions abstract both ideas. This is, however, not unimportant (not to suggest I think @10000truths said so, exactly). In educational settings one usually wants to begin with the most familiar examples and then generalize. { Why, this probably even applies to greats like Russell. :-) } Further, in attributional settings, giving general names/notions to things is often less seminal than the things one is naming. (Both are often worthy of attention, but I tend to push back when "namers get all the credit".) There is probably no single, famous big name like Russell to attach to the idea of units of measure/standard conversion/comparison. There may be a King of Olden Times who beheaded those who didn't follow his particular "system" when taxing crop growing areas or converting area to expected weights or volumes of grain/etc. ;-) In some ways the very idea of "money" itself incorporates standardized exchange/comparison within it. Money itself is taken to be pre-historic [1], though there may have been a few original "coins"/tokens of money. Little tick marks in clay ledgers may have been the first and we can be fairly sure even before all the spice trade/wars that not all crops/goods were deemed equal/additive unconverted. On the contrary, money was useful specifically to help convert. [1] https://en.wikipedia.org/wiki/History_of_money https://en.wikipedia.org/wiki/History_of_money
gimboland 5y ago
I had that realisation when I saw this library: https://pint.readthedocs.io/en/stable/ https://pint.readthedocs.io/en/stable/ (for a dynamically typed language, somewhat amusingly).

by cb321 5y ago

tel 5y ago

Yeah, saying Russell invented types is fun but horribly wrong. He invented other things and stood at the center of an explosion in formal logics. But types are way old.

JoBrad 5y ago
Maybe he invented it the way that many people think the color blue was invented? Causing everyone to see something for the first time (especially when it was right under our noses) is certainly impressive.
- EarthLaunch 5y ago
  In my game design I've imagined two parallels to invention; discovery and identification. All three are learning about the world, but in slightly different ways. Invention: I created that. Discovery: I found that lying around. Identification: I conceptualized a definition for that.
- tel 5y ago
  This is certainly more true. That explosion of logics I mentioned was a big movement of many authors to expand our understanding of types (among other things).
titzer 5y ago
When people say a mathematician "invented" something, it's understood that they didn't create it from nothing. Newton didn't "invent" gravity, for example, he just came up with the first mathematically rigorous theory for it. Same for Russell and types.
- wlib 5y ago
  This shows a funny way that the word invent has shifted in meaning. Invent means “found” (almost literally “came upon” in Latin) - yet for some reason it shifted to mean “created” in a sort of “this is mine don’t steal it from me” sense. Then here we are clarifying that we literally mean the actual meaning of the word. It’s interesting that math is considered impossible to have as intellectual property, yet we think somehow that IP law is justifiable for everything else.
  - titzer 5y ago
    Yeah, that is odd. The german word is "erfunden" which is something like "completely found".
  - Koshkin 5y ago
    > we literally mean the actual meaning Also, in the everyday speech the word "literally" no longer means what it was meant to mean.
- tel 5y ago
  I understand that distinction. Russell came up with a mathematically rigorous theory for the foundations of mathematics and happened to use a very simple type system to accomplish it. He wasn't the first to formally make use of types, though he may have been the first to use that term. He also seriously pushed forward our techniques of mathematical rigor, so in some sense he "invented" many, many, many things. To be clear, I think Russell was an amazing mathematician and inventor. I also think that the history of types is way more rich and interesting than just saying that he invented the idea. To not mention at least Frege is to miss a lot.

Aerroon 5y ago

I had never thought of type systems in this way. If type systems are effectively a "unit" attached to the data then you can think of them as an unknown value in arithmetic. Eg "4x + 4y = 40.4z" x, y, and z here are units: x is meters, y is centimeters, and z is decimeters. You could do the same with types. The computer only knows the binary value, but the type assigns meaning to the value just like physical units do. This must've been really obvious to a lot of people, but it only clicked just now for me. Thank you.

kroltan 5y ago
By analogy, that's also how type inference works. If you know X, and either the type-rules for arithmetic, or Z, you can figure out Y. The constraints of their usage can be used to determine the type required of that data.
10000truths 5y ago
I think of it the other way around - dimensional analysis of units is a special case of a type system. Two units of different measures cannot be added/subtracted with one another. Units of the same measure (e.g. length: cm, in) are trivially convertible via a scalar factor (e.g. 2.54 cm/in), and units of different measures (e.g. length: m, time: s) can be multiplied/divided to get a new unit of measure (speed: m/s), although some such units might have no practical use.
- cb321 5y ago
  Dimensional analysis of units is absolutely a special case (I said "primordial example") of type systems. Proof: "constrained operations" and "notional objects" are very limited/somewhat concrete - "additive/comparative/conversion-y" and "measured things". Modern notions abstract both ideas. This is, however, not unimportant (not to suggest I think @10000truths said so, exactly). In educational settings one usually wants to begin with the most familiar examples and then generalize. { Why, this probably even applies to greats like Russell. :-) } Further, in attributional settings, giving general names/notions to things is often less seminal than the things one is naming. (Both are often worthy of attention, but I tend to push back when "namers get all the credit".) There is probably no single, famous big name like Russell to attach to the idea of units of measure/standard conversion/comparison. There may be a King of Olden Times who beheaded those who didn't follow his particular "system" when taxing crop growing areas or converting area to expected weights or volumes of grain/etc. ;-) In some ways the very idea of "money" itself incorporates standardized exchange/comparison within it. Money itself is taken to be pre-historic [1], though there may have been a few original "coins"/tokens of money. Little tick marks in clay ledgers may have been the first and we can be fairly sure even before all the spice trade/wars that not all crops/goods were deemed equal/additive unconverted. On the contrary, money was useful specifically to help convert. [1] https://en.wikipedia.org/wiki/History_of_money https://en.wikipedia.org/wiki/History_of_money

gimboland 5y ago

I had that realisation when I saw this library: https://pint.readthedocs.io/en/stable/ https://pint.readthedocs.io/en/stable/ (for a dynamically typed language, somewhat amusingly).