Hacker News Reader

Comment by hyperpape | Hacker News Reader

Right or wrong, simply saying something is poorly named doesn't show that someone is hostile towards academia. By that standard, most of the academics I know would be hostile to academia, since they invariably think something in their field has a bad name.

View on HN

I'm just miffed that they're complaining about names that are actual words. How would you like if they were all named after their discoverers, and therefore an a priori undistinguished mishmash of proper names? (cf. separation axioms[1])

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

That's pretty funny. I'm sure memorizing the differences between the Hausdorff, the completely Hausdorff, the regular Hausdorff, the normal Hausdorff, the completely normal Hausdorff, and the perfectly normal Hausdorff must be fun.

There are only two hard things in Computer Science: cache invalidation and naming things. —Phil Karlton

oh, and:

The first step towards wisdom is calling things by their right names. —Anonymous Chinese Proverb

There are only two hard things in Computer Science: cache invalidation, naming things, and off-by-1 errors.

It doesn't help to use "actual words" when those words have no discernible relationship to their usage. And I don't just mean "common" usage, but the usage by others in related fields. "affine" and "linear" are commonplace concepts in mathematics, but it is in no way clear how they relate to type systems, let alone what properties a type system has when described as such.

The only other fields I know of where things are as badly named are are abstract algebra (ideal, ring, module) and grammar (infinitive, perfect, accusative). It seems to be no coincidence that type theory straddles the two.

Simply saying it is poorly named doesn't, but this sentence:

"Just so you can look this stuff up in The Literature, I'll be providing all these bad names with a Trademark of Disdain™, but otherwise I'd prefer to use Rust-centric terminology." pretty clearly does.

The TM thing is obnoxious.

I think it's it hilarious (and true that academia often chooses poor names).

Yeah, it would be better with coloring. Or better yet hyperlinking to the relevant Wikipedia pages / papers / memes.

Edit: pages such as https://en.wikipedia.org/wiki/Idempotency_of_entailment, https://en.wikipedia.org/wiki/Monotonicity_of_entailment, https://en.wikipedia.org/wiki/Structural_rule, https://en.wikipedia.org/wiki/Nice_guy, https://en.wikipedia.org/wiki/Linear_logic, https://en.wikipedia.org/wiki/Affine_logic, https://en.wikipedia.org/wiki/Relevance_logic (not sure why "Proper Support" is capitalized, that seems to have no referent)

Hyperlinks allow you to directly look up a term by clicking on it, i.e. are actually useful, whereas trademark symbols are just visual noise. Although of course it is possible to over-link as well, see e.g. the wiktionary FAQ on "wikifying": https://en.wiktionary.org/wiki/Help:FAQ#Wikifying, in practice this doesn't seem to happen; it's more the reverse problem of not putting in enough links.

Literally the only link in the article, on the first use of the Official Terminology, is a link to the wikipedia page that defines all the terms.

And that's not really sufficient; words have a life of their own and take on contextual meanings outside of whatever scope they're introduced in. Case in point, linear types come from linear logic, by Girard, whereas relevant types come from unrelated older work by Belnap and Anderson. The simple act of putting them under one umbrella term, "substructural types", erases the older work and means that the article will focus more on Girard's perspective of logic.

Then the article makes the "discovery" that "People who say they want Linear™ Types In Rust actually just want Proper Support For Relevant™ Types.", which is pretty obvious if you know this historical context, and coins yet another term, must-use types, which unsurprisingly has no ™ after it.

I think I get what you're trying to do, I myself used ™ for a little bit back 6-7 years ago, a little bit before I wrote http://insearchoftheultimateprogramming.blogspot.com/2011/04.... But ™ just isn't effective; even if you think you know what a term means, you can't explain it except by its relationship to other terms. And once you forget what that ™ symbol referred to you're just as clueless as everyone else. Whereas URLs are "resource locators" and actually clarify what you intended.

The bit about erasing seems like a bit of stretch. Belnap taught at least one of his proof theory classes using Restall's "An Introduction to Substructural Logics" as a textbook. (Belnap did make it clear that he didn't think linear logic was relevant to his own philosophical concerns, but that's not the same as saying he bears it some kind of ill-will).

Well, if relevance logic is part of linear logic, and it's a true subsumption relationship, then you're saying Belnap doesn't think relevance logic is relevant anymore. So in other words he's pretty much rejected logic altogether.

I guess it makes sense, his most recent papers are about indeterminism (http://www.pitt.edu/~belnap/futurecontingents.pdf), which logic doesn't handle well, but I'm not quite sure how you'd represent the branching-universe model he uses in a type system. I guess you'd need the history operator he uses, m/h = moment m on history h.

I was referring to the subsumption under substructural logic, not a subsumption under linear logic. Belnap seemed to view linear logic as rather different from his own interests in relevance logic.

Reply on news.ycombinator.com