4 ms·

One of those rare comments that I can't intuit the meaning of even though I know the definitions of all the words. In so far as this is math, this is completely

One of those rare comments that I can't intuit the meaning of even though I know the definitions of all the words. In so far as this is math, this is completely, perfectly, thoroughly, abstract. So in reality did you mean to say reified ie made concrete? Or did you mean to say obviated ie made irrelevant? And you think computer science did this? The thing where the point of the game is to build more and more abstract representations of things? Like what do you think the word "abstracted" actually means?

JadeNB 3y ago
It seems clear enough to me what the GP might have meant, at least clear enough that it need not be responded to with remarks like "Like what do you think the word "abstracted" actually means?" that reads to me as saying that, whatever the GP thinks, it is wrong. Type notation presumably started off as a very concrete thing—probably just about anyone can read something like BOOL = TRUE | FALSE. But then—I'm speaking here from a general perspective of computer-theoretic notation, so it's entirely possible that these are not actual notations that occur in type theory—things were added like syntactic sugar, say, for character classes, about whose abstract-ness we can argue but which definitely adds a decoding layer for people not used to it; and things like parametrized types/higher types that very definitely do add abstraction. It's very likely that, almost any time a definition benefits from an extra side remark, "For example, …", it is illustrating an additional abstraction.
- mathisfun123 3y ago
  >that reads to me as saying that, whatever the GP thinks, it is wrong. let me give you an example sentence and you tell me if the word "abstracted" makes sense, in context: "the accounting spreadsheet abstracts away all of the calculus because all the numbers are written down exhaustively"
  - JadeNB 3y ago
    > let me give you an example sentence and you tell me if the word "abstracted" makes sense, in context: > "the accounting spreadsheet abstracts away all of the calculus because all the numbers are written down exhaustively" I'm not even sure what the meaning is supposed to be, because I would not expect to use a spreadsheet to do calculus. (Of course there are ways of forcing calculus into a spreadsheet, but I wonder if you just meant 'calculation'.) Here I would say that it is absolutely relevant to speak of a spreadsheet abstracting away the details of a computation: the logic of the spreadsheet will probably refer often to the contents of cells, without worrying about what the contents are, and that is very definitely a kind of abstraction. I would certainly not call the process of entering numbers into a spreadsheet an abstraction; but it seems to be the opposite of what type theory does. For example, type theory allows general reasoning about families of types, without reasoning case by case for each individual one. This seems to be the very essence of abstraction (in which capacity it is, conceptually, not completely distinct from the formulas in a spreadsheet). If you see no abstraction, only concreteness, in type-theory notation, I suspect that is more an indication that you have learned to see through the abstraction than that it isn't there.
    - mathisfun123 3y ago
      >This seems to be the very essence of abstraction yes and that's exactly my point... how does it make sense to utter the sentence "this has been abstracted [away]" when the `this` is itself the essence of abstraction. i'm not really sure how people aren't getting what i'm putting down here: type theory can't be abstracted away because type theory itself is the thing that does the abstracting.
      - JadeNB 3y ago
        > how does it make sense to utter the sentence "this has been abstracted [away]" when the `this` is itself the essence of abstraction. I think that you and I are reading this sentence (https://news.ycombinator.com/item?id=37140437 https://news.ycombinator.com/item?id=37140437) differently: > > It’s a testament to computer science that this has been so thoroughly abstracted over the years As your brackets indicate, you are reading a word "[away]" that is not explicitly present in the text. It seems to me to make more sense to read it without adding "away". (Wiktionary, for example, does not require that, or any, preposition in sense 6 of https://en.wiktionary.org/wiki/abstract#Verb https://en.wiktionary.org/wiki/abstract#Verb, which is the one that seems to me to fit here.) For example, I am a mathematician, and I could say that mathematics has been abstracted over the years (millennia!). I do not mean that the mathematics has been abstracted away, which I agree with you would be in some sense meaningless, but rather that the mathematics itself has literally been abstracted: from only being able to count and do arithmetic with specific real-world objects, to being able to do count and do arithmetic with numerals that did not refer to a specific thing, to being able to use letter to refer to numerals of unknown or variable value, to … well, there's not such a clear linear progression after that, but there's definitely a tower of abstraction. I hope that this sense of "mathematics has been thoroughly abstracted over the years" is an intelligible one (even if phrased differently from the way I assume you, or perhaps even I, might phrase it ourselves). It is in that sense that I take the sentence "It’s a testament to computer science that this [meaning, I think, notation in type theory] has been so thoroughly abstracted over the years".
hathawsh 3y ago
The comment is praise for maintaining compatibility. To me, the sentence "It’s a testament to computer science that this has been so thoroughly abstracted over the years" means: "It’s a testament to computer science that the original notation has been successfully applied to many things without drastic changes". I don't know whether that is one of the standard definitions of the past tense verb "abstracted", but it's a common usage in software engineering.
- mathisfun123 3y ago
  > has been successfully applied to many things without drastic changes. but it's a common usage in software engineering. give me an example sentence. let me try one: "<protobufs> have been abstracted over the years because they have been applied to many things without drastic changes". doesn't work the only way in which "abstracted" is used in SWE is "abstracted away" or "abstracted out", which means ~the details aren't important or ~it's being handled by someone/something else for you. having written out this response i am now 100% sure it's the former in this case. no one seems to get that what i'm making fun of here is this person reveling in the fact that they don't have to understand type theory "like our forefathers did" but then stating that fact using theory speak. it's like which is it: do you care about abstractions and abstracting things out (and thus should be fine with type theory) or are you a blue collar dev that just copy-pastes. you can't have it both ways (certainly you might try but this leads to the cognitive dissonance on display here).

JadeNB 3y ago

It seems clear enough to me what the GP might have meant, at least clear enough that it need not be responded to with remarks like "Like what do you think the word "abstracted" actually means?" that reads to me as saying that, whatever the GP thinks, it is wrong. Type notation presumably started off as a very concrete thing—probably just about anyone can read something like BOOL = TRUE | FALSE. But then—I'm speaking here from a general perspective of computer-theoretic notation, so it's entirely possible that these are not actual notations that occur in type theory—things were added like syntactic sugar, say, for character classes, about whose abstract-ness we can argue but which definitely adds a decoding layer for people not used to it; and things like parametrized types/higher types that very definitely do add abstraction. It's very likely that, almost any time a definition benefits from an extra side remark, "For example, …", it is illustrating an additional abstraction.

mathisfun123 3y ago
>that reads to me as saying that, whatever the GP thinks, it is wrong. let me give you an example sentence and you tell me if the word "abstracted" makes sense, in context: "the accounting spreadsheet abstracts away all of the calculus because all the numbers are written down exhaustively"
- JadeNB 3y ago
  > let me give you an example sentence and you tell me if the word "abstracted" makes sense, in context: > "the accounting spreadsheet abstracts away all of the calculus because all the numbers are written down exhaustively" I'm not even sure what the meaning is supposed to be, because I would not expect to use a spreadsheet to do calculus. (Of course there are ways of forcing calculus into a spreadsheet, but I wonder if you just meant 'calculation'.) Here I would say that it is absolutely relevant to speak of a spreadsheet abstracting away the details of a computation: the logic of the spreadsheet will probably refer often to the contents of cells, without worrying about what the contents are, and that is very definitely a kind of abstraction. I would certainly not call the process of entering numbers into a spreadsheet an abstraction; but it seems to be the opposite of what type theory does. For example, type theory allows general reasoning about families of types, without reasoning case by case for each individual one. This seems to be the very essence of abstraction (in which capacity it is, conceptually, not completely distinct from the formulas in a spreadsheet). If you see no abstraction, only concreteness, in type-theory notation, I suspect that is more an indication that you have learned to see through the abstraction than that it isn't there.
  - mathisfun123 3y ago
    >This seems to be the very essence of abstraction yes and that's exactly my point... how does it make sense to utter the sentence "this has been abstracted [away]" when the `this` is itself the essence of abstraction. i'm not really sure how people aren't getting what i'm putting down here: type theory can't be abstracted away because type theory itself is the thing that does the abstracting.
    - JadeNB 3y ago
      > how does it make sense to utter the sentence "this has been abstracted [away]" when the `this` is itself the essence of abstraction. I think that you and I are reading this sentence (https://news.ycombinator.com/item?id=37140437 https://news.ycombinator.com/item?id=37140437) differently: > > It’s a testament to computer science that this has been so thoroughly abstracted over the years As your brackets indicate, you are reading a word "[away]" that is not explicitly present in the text. It seems to me to make more sense to read it without adding "away". (Wiktionary, for example, does not require that, or any, preposition in sense 6 of https://en.wiktionary.org/wiki/abstract#Verb https://en.wiktionary.org/wiki/abstract#Verb, which is the one that seems to me to fit here.) For example, I am a mathematician, and I could say that mathematics has been abstracted over the years (millennia!). I do not mean that the mathematics has been abstracted away, which I agree with you would be in some sense meaningless, but rather that the mathematics itself has literally been abstracted: from only being able to count and do arithmetic with specific real-world objects, to being able to do count and do arithmetic with numerals that did not refer to a specific thing, to being able to use letter to refer to numerals of unknown or variable value, to … well, there's not such a clear linear progression after that, but there's definitely a tower of abstraction. I hope that this sense of "mathematics has been thoroughly abstracted over the years" is an intelligible one (even if phrased differently from the way I assume you, or perhaps even I, might phrase it ourselves). It is in that sense that I take the sentence "It’s a testament to computer science that this [meaning, I think, notation in type theory] has been so thoroughly abstracted over the years".

hathawsh 3y ago

The comment is praise for maintaining compatibility. To me, the sentence "It’s a testament to computer science that this has been so thoroughly abstracted over the years" means: "It’s a testament to computer science that the original notation has been successfully applied to many things without drastic changes". I don't know whether that is one of the standard definitions of the past tense verb "abstracted", but it's a common usage in software engineering.

mathisfun123 3y ago
> has been successfully applied to many things without drastic changes. but it's a common usage in software engineering. give me an example sentence. let me try one: "<protobufs> have been abstracted over the years because they have been applied to many things without drastic changes". doesn't work the only way in which "abstracted" is used in SWE is "abstracted away" or "abstracted out", which means ~the details aren't important or ~it's being handled by someone/something else for you. having written out this response i am now 100% sure it's the former in this case. no one seems to get that what i'm making fun of here is this person reveling in the fact that they don't have to understand type theory "like our forefathers did" but then stating that fact using theory speak. it's like which is it: do you care about abstractions and abstracting things out (and thus should be fine with type theory) or are you a blue collar dev that just copy-pastes. you can't have it both ways (certainly you might try but this leads to the cognitive dissonance on display here).