Hacker News Reader

Comment by cb321 | Hacker News Reader

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.

View on HN

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.

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.

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.

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

Perhaps the fundamental dimension (mass, length, time etc.) could be considered as the 'abstract base class', with the specific units (meters, feet...) being derived classes.

Perhaps. The https://en.wikipedia.org/wiki/Buckingham_%CF%80_theorem and Lord Rayleigh's refined ideas on units of measure predated Russell's work. These ideas also include at least 1 abstract-to-specialized transform like @HPSquared suggests. Probably it was >1 transform in the sense that (Mass, Length, Time) are conventional not fundamental.

Following up on that ">1" requires a bit of explanation. Particle physics gets by with "natural" units where basically everything is rational powers of one base unit (MeV|energy|whatnot). SI units want like 7 or 8 or 9 base dimensions to avoid fractional powers (kind of a losing game since as soon as you have an equation with varying integer powers on either side fractional powers resurface).

Rayleigh may have used different English words than "abstract base class" or "type" (maybe "kind", "sort", etc.), but physicists definitely had "type ideas" more abstract and formally symbolic than the units of measure your grandma knew for recipes - before Russell said anything about them.

I am not sure Planck was the first to realize the "pick how many base dimensions you want" tricks - seems like Rayleigh or even earlier may have been, but in 1899 Planck published (before Russell's 1903 Doctrine of Types) a very abstract system of units such that major constants are 1.0 and dimensionless [1]. That level of conceptual abstraction (dimensionality - at least 1 more than just concrete vs abstract) also clearly predated Russell - but maybe only by a decade or two.

It seems to me uncontentious that physics/physicists were in a very abstract type theory headspace with regard to units of measure before Russell published that appendix. The only point of debate would be "Does it count or did Russell abstract it so much further as to count as a fundamentally different thing?" While I am no Russell biographer, it would be unsurprising to me if he was inspired either implicitly or even very explicitly by such "just earlier than him" happenings in physics like Planck units. These units famously "make physics look more like pure math" which does not seem like something Russell would have failed to notice.

As an "error catching mechanism" like types in programming languages, units function exactly the same way as programming types - just with the person as a compiler "doing their own checksum" to make sure they don't add apples & oranges. Calculation by hand was the predominant kind of computation at the time. So this is all coherent. At least "along the history of ideas arc" leading to programming language types, there may be great abstracters, but I doubt credit can be given to one person like TFA article tries to except maybe as an ambassador/evangelist/namer/maaaaybe first abstractor. (Not trying to suggest realizing the importance of something doesn't matter, but more make people realize how much this particular line of thought is almost as prehistoric as numbers themselves/quantification itself.)

Anyway, I find units for mass, speed, time, etc. useful in explaining types (and checksums) to non-programmers. Maybe you will, too.

[1] https://en.wikipedia.org/wiki/Planck_units

> and units of different measures (e.g. length: m, time: s)

A nitpick but those are also related by a simple scalar factor (the speed of light)

This is exactly correct. And once you think of it as the variable, you can then make the leap to thinking about it as dimensions, which has some nice properties in physics i.e. vector addition/subtraction leads to tuples of dimensions, while the product doesn't - which explains why we can't add/subtract different units, but we can multiple them together.

Check out Frink[1] and my recreation of a similar language, Farnsworth[2]

[1] https://frinklang.org/ [2] https://metacpan.org/pod/Language::Farnsworth

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.

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.

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.

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).

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.

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.

Yeah, that is odd. The german word is "erfunden" which is something like "completely found".

> we literally mean the actual meaning

Also, in the everyday speech the word "literally" no longer means what it was meant to mean.

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.

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

Reply on news.ycombinator.com