4 ms·

To anyone hesitating to read this: it's an explanation of type system notation in Computer Science papers, basically a primer on BNF notation, inference rules,

by the_af 3y ago

To anyone hesitating to read this: it's an explanation of type system notation in Computer Science papers, basically a primer on BNF notation, inference rules, etc for type systems. It looks like a good summary.

dclowd9901 3y ago
Honestly, I just need a cheat sheet for how to read the symbols using english words. I understand the concepts of the logical application of typing, but I don't read computer science dissertations regularly enough to make them the mapping of symbols to meaning stick.
- yawpitch 3y ago
  > Honestly, I just need a cheat sheet for how to read the symbols using english words. Amen… however I believe the existence of such a cheat sheet would represent an existential economic risk for PLT researchers, and they’d be incentivized to add more Greek (and, eventually, Cyrillic, then Czech, then eventually Xhosa and probably Klingon) symbols in order to retain access to funding. It’s only a matter of time before someone reinvents the paper town inside of PLT papers, if they haven’t already.* * the above is meant to be taken facetiously > I understand the concepts of the logical application of typing, but I don't read computer science dissertations regularly enough to make them the mapping of symbols to meaning stick. I just wish CS (and, indeed, mathematics) was even remotely internally consistent… cross the boundaries between any two extremely narrow domains and ω can mean anything. It’s (very) vaguely consistent within PLT, but even there getting lowercase omega “stuck” in your head as having one English translation is just a pathway to pain.
- Twisol 3y ago
  I read `A |- x : t` as "In context A, x has type t". An entire inference rule (i.e. the horizontal bar separating some premises from a conclusion) is read as as "if P, Q, ... hold, then R holds"; or, sometimes, "We obtain R if we have P, Q, ...".
  - Tainnor 3y ago
    That works if typing rules are unambiguous. But you might have |- x : t1, as well as |- x :t2 (for example, numeric literals in Haskell can have several types). Instead of saying "x has type t", one could think of it as "x can be inferred to be of type t" or "we can derive/prove that x has type t". The latter mirrors the usage in formal logic where the turnstyle symbol generally is used to mean "is provable".
    - Twisol 3y ago
      This is all true, although nothing about the reading "x has type t" implies that "x" can only have one type. It is a separate metatheorem about your system of inference rules that terms have unique types -- and not even one that is always true, e.g. in the presence of subtyping. > for example, numeric literals in Haskell can have several types Technically, numeric literals in Haskell have precisely one type: `(Num a) => a`. The literal `42` is actually interpreted as the expression `fromInteger (42 :: Integer)`, where `fromInteger` is a function on the `Num` typeclass. In turn, the `Num` typeclass constraint desugars to a function taking a dictionary of functions, `NumDict a -> a`. The typeclass machinery just means GHC will infer the appropriate instance whose dictionary should be provided. (technically technically, GHC can be even cleverer if it knows statically which dictionary will be used, avoiding using the dictionary entirely; but this desugaring to dictionaries is ground truth, semantically.)
      - deleted 3y ago
        [deleted]
ljm 3y ago
It’s a testament to computer science that this has been so thoroughly abstracted over the years
- mathisfun123 3y ago
  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"

by the_af 3y ago

dclowd9901 3y ago

Honestly, I just need a cheat sheet for how to read the symbols using english words. I understand the concepts of the logical application of typing, but I don't read computer science dissertations regularly enough to make them the mapping of symbols to meaning stick.

yawpitch 3y ago
> Honestly, I just need a cheat sheet for how to read the symbols using english words. Amen… however I believe the existence of such a cheat sheet would represent an existential economic risk for PLT researchers, and they’d be incentivized to add more Greek (and, eventually, Cyrillic, then Czech, then eventually Xhosa and probably Klingon) symbols in order to retain access to funding. It’s only a matter of time before someone reinvents the paper town inside of PLT papers, if they haven’t already.* * the above is meant to be taken facetiously > I understand the concepts of the logical application of typing, but I don't read computer science dissertations regularly enough to make them the mapping of symbols to meaning stick. I just wish CS (and, indeed, mathematics) was even remotely internally consistent… cross the boundaries between any two extremely narrow domains and ω can mean anything. It’s (very) vaguely consistent within PLT, but even there getting lowercase omega “stuck” in your head as having one English translation is just a pathway to pain.
Twisol 3y ago
I read `A |- x : t` as "In context A, x has type t". An entire inference rule (i.e. the horizontal bar separating some premises from a conclusion) is read as as "if P, Q, ... hold, then R holds"; or, sometimes, "We obtain R if we have P, Q, ...".
- Tainnor 3y ago
  That works if typing rules are unambiguous. But you might have |- x : t1, as well as |- x :t2 (for example, numeric literals in Haskell can have several types). Instead of saying "x has type t", one could think of it as "x can be inferred to be of type t" or "we can derive/prove that x has type t". The latter mirrors the usage in formal logic where the turnstyle symbol generally is used to mean "is provable".
  - Twisol 3y ago
    This is all true, although nothing about the reading "x has type t" implies that "x" can only have one type. It is a separate metatheorem about your system of inference rules that terms have unique types -- and not even one that is always true, e.g. in the presence of subtyping. > for example, numeric literals in Haskell can have several types Technically, numeric literals in Haskell have precisely one type: `(Num a) => a`. The literal `42` is actually interpreted as the expression `fromInteger (42 :: Integer)`, where `fromInteger` is a function on the `Num` typeclass. In turn, the `Num` typeclass constraint desugars to a function taking a dictionary of functions, `NumDict a -> a`. The typeclass machinery just means GHC will infer the appropriate instance whose dictionary should be provided. (technically technically, GHC can be even cleverer if it knows statically which dictionary will be used, avoiding using the dictionary entirely; but this desugaring to dictionaries is ground truth, semantically.)
    - deleted 3y ago
      [deleted]

ljm 3y ago

It’s a testament to computer science that this has been so thoroughly abstracted over the years

mathisfun123 3y ago
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"