8 ms·
How should I read type system notation?
- nicechianti 3y ago[dead]
- the_af 3y agoTo 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 agoHonestly, 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 agoI 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 agoThat 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 agoThis 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 agoIt’s a testament to computer science that this has been so thoroughly abstracted over the years
- mathisfun123 3y agoOne 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 agoIt 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"
- idreyn 3y agoLovely. I've wondered about this for years but never knew quite how to frame a query to learn more.
- armchairhacker 3y agoThis is a nice explanation, but why is it written on stack exchange and not (also?) https://lexi-lambda.github.io/ https://lexi-lambda.github.io/?
- IshKebab 3y agoI guess because StackExchange has higher Google ranking and allows comments, easy edits, supports latex etc. It's a great platform for stuff like this.
- DylanSp 3y agoAlso, the langdev SE is still in beta, and pretty early beta at that; posting useful material there helps get it off the ground. That said, I wouldn't be surprised if Alexis also posts it to her blog at some point.
- the_af 3y agoThe person who wrote this [1] seems to be a Haskell (GHC) contributor and someone hailing from lexi-lambda. ---- [1] https://langdev.stackexchange.com/users/861/alexis-king https://langdev.stackexchange.com/users/861/alexis-king
- lcnPylGDnU4H9OF 3y agoWhere could one find an example of this notation “in the wild”?
- UncleMeat 3y agoProceedings in POPL or PLDI will have plenty of papers with this stuff.
- ratmice 3y agoIt is used in The definition of Standard ML to define the syntax and semantics of the language. That is the most "in the wild" usage I'm familiar with in the sense that it gives a formal specification of the language, which has been used across multiple implementations of the language successfully... https://smlfamily.github.io/sml90-defn.pdf https://smlfamily.github.io/sml90-defn.pdf
- agalunar 3y agoThis seems like maybe a right place to evangelize [1] the only hill I've decided to die on: the formatting of type annotations that use a colon in their syntax. Specifically, there should be an equal amount of space on both sides of the colon. I keep meaning to write a proper essay, but this is the essential argument. I think of it this way: there are two symbols that by coincidence are written the same (two aligned dots). I mean that genuinely (as in, I actually think of them as separate things), but it also helps as an explanative device. The first I'll call the prefatory or label(ing) colon. Its usage matches usage in English [2], where the text preceding the colon introduces the text after the colon, or the thing on the left is a label or name for the thing on the right. For example, it is used to start a block (as in Python), or to define a key-value pair, or define a name-value pair in a struct (as in C or Rust). The second is the type annotation. This syntax is borrowed from mathematics. It is a binary relation, and binary relations are written with equal space on the left and right. Just as you'd never write "x= 1" (another relation), "x> y" (relation), or "x+ z" (operator), you'd never write "x: X". Instead you write "x = 1", "x > y", and "x + z" or "x+z" instead. Whenever I see "a: b", I immediately think labeling colon. Despite having seen it thousands of times, I always have to perform an additional mental step (however trivial) when it turns out to be a type annotation; it takes a small amount of mental energy to dismiss each instance of syntax that looks wrong. [Truthfully, I'm somewhat baffled how it would ever even cross anyone's mind when designing a language to write type annotations like "x: X" given the long-established, pre-existing precedent in mathematics and the way its semantics seem backwards (if you had to use a labeling colon, "X: x" would make much more sense to me).] edit: I should be explicit that I'm referring to programming language syntax, and that I much prefer "x : X" over "X x" (there are good reasons I think for the type to be on the right-hand side, but other people have already written about that). [1] "Evangelion" is a really lovely word, from εὐαγγέλιον good news = εὐ- good + ἄγγελος messenger, the double gamma pronounced even in ancient Greek as "ŋg" ("ng") rather than "ːg" ("g"). [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_English https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...
- dvt 3y agoPretty sure it's standard practice to always do "t[space]:[space]T" with equidistant spaces between the colon. In spite of Type Theory generally being an inconsistent mess, this is a rare case where everyone seems to be fairly consistent. I was actually curious how I did it in undergrad, and even I had the common-sense of making it look nicely symmetrical[1] :) [1] https://dvt.name/logic/horse2.pdf https://dvt.name/logic/horse2.pdf
- deleted 3y ago[deleted]
- dan-robertson 3y agoThere was a Guy Steele talk a while ago on this topic. He also gives searchable names for some of the things (eg the ‘2d inference rule diagrams’). He calls it ‘computer science metanotation’, though I think it’s more of a PLT thing. https://m.youtube.com/watch?v=dCuZkaaou0Q https://m.youtube.com/watch?v=dCuZkaaou0Q
- deleted 3y ago[deleted]
- carapace 3y agoYou beat me to it. > The most popular programming language in computer science has no compiler, interpreter, or complete specification. It is remarkably concise. It grew over decades; today, dozens of variations are in use. Its complexity has reached the point where it needs to be re-explained every time it is used—but too often it is not; instead, each variant is more or less taken for granted. This has led to ambiguities and inconsistencies. Much effort has been spent in hand-translating, in both directions, between this language and other languages that do have compilers, primarily for the purpose of implementing yet other languages. => https://en.wikipedia.org/wiki/Guy_Steele https://en.wikipedia.org/wiki/Guy_Steele Guy Steele => https://www.codemesh.io/codemesh2017/guy-l-steele https://www.codemesh.io/codemesh2017/guy-l-steele "A Cobbler's Child" talk at Code Mesh 2017 => https://www.youtube.com/watch?v=qNPlDnX6Mio https://www.youtube.com/watch?v=qNPlDnX6Mio "A Cobbler's Child" (video on youtube) => https://www.youtube.com/watch?v=dCuZkaaou0Q https://www.youtube.com/watch?v=dCuZkaaou0Q "It's Time for a New Old Language" (video on youtube) => https://news.ycombinator.com/item?id=15473199 https://news.ycombinator.com/item?id=15473199 Discussion on HN => https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150_PUBLICATION_ID:5376 https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150... Slides To me this seems like a pretty sorry state of affairs. The folks trying the hardest to speak precisely about the most precise human art use ambiguous and inconsistent notation. wat?
- nextaccountic 3y agoThis is also the notation that is used in logic as well. The thing about it is that, while every paper can have a slightly different variant of this metalanguage, all texts are supposed to contain an introduction defining exactly what this means. That's because it's common that, if you are talking about a new logic, you will have new syntax as well, or a slightly different way to make inference
- eirikbakke 3y ago"Types and Programming Languages" by Benjamin C. Pierce is a good textbook that covers this kind of stuff.
- thechao 3y agoTAPL is remarkably unclear on the basic meaning of the syntax it uses; which I find ironic. This answer is orders-of-magnitude clearer than TAPL.
- OJFord 3y agoAgreed, I stumbled through a course on essentially TAPL at university, and bought & read Pierce's TAPL to help. It's a great book, but the submission would've helped me a lot as an additional primer. I didn't have the background in mathematical logic for it frankly. (It was a third of fourth year CS course, but where everyone else would've had more formal logic in first and second, I'd had the electronics part of my programme, which was actually based in EE. I naïvely thought I'd read enough to have the requisite background and I absolutely hadn't, or at least not to understand & follow fast enough.)
- kfixjviv 3y agoSee also: https://www.hedonisticlearning.com/posts/understanding-typing-judgments.html https://www.hedonisticlearning.com/posts/understanding-typin...
- imrehg 3y agoFrom the examples: > 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 means “𝗍𝗋𝗎𝖾+2 has type 𝖨𝗇𝗍”, which makes even less sense, as the expression 𝗍𝗋𝗎𝖾+2 is nonsense and does not have any type at all. Well, Python called where `True + 2` is actually an int and is equal to 3. :) This doesn't say anything about whether this should be the case or not, just whether it is.
- edgyquant 3y agoIsn’t this language specific? For instance in C doesn’t true map to 1, thus true+1=2
- Tainnor 3y agoThe runtime values don't matter to type theory, only the types of expressions.
- dreamcompiler 3y agoEven though 'True + 2' doesn't throw an error in Python or C, it's still stupid because it makes the semantics of the language hard to reason about, in order to give programmers a little syntactic sugar.
- anttihaapala 3y agoThis is for backward-compatibility reasons. The comparison operators in Python produced 1 or 0 before boolean was a thing, and programs existed that exploited this, i.e. you can do something like `(a < b) - (a > b)` in a sorting algorithm. Same thing in C, or even more so, as the comparison operators produce an `int` instead of a `bool`.
- logicchains 3y ago>Even though 'True + 2' doesn't throw an error in Python or C, it's still stupid because it makes the semantics of the language hard to reason about It's consistent. If we add a 64 bit integer and a 32 bit integer, we'd expect to get a 64 bit integer as the result. Same with if we add a 64 bit integer and a 4 bit integer. So why shouldn't it also apply if we add a 64 bit integer and a 1 bit integer? Mathematically, bool is a 1-bit integer with fancy names for 1 and 0.
- kitanata 3y ago[flagged]
- deleted 3y ago[deleted]
- ajdude 3y agoWhen I was reading the Ada Reference Manual[1], I immediately recognized this kind of syntax. I didn't actually know what it was called, but it's interesting to see it in practical use. The whole language is defined in that kind of notation. [1] For example: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax
- Jtsummers 3y agohttp://www.ada-auth.org/standards/22rm/html/RM-1-1-4.html http://www.ada-auth.org/standards/22rm/html/RM-1-1-4.html The Ada Reference Manual specifies the notation they use. They're using a variant of Backus-Naur Form and they describe their particular variant in the section I linked above.
- mbwgh 3y agoThe notation goes back to Frege. It's not easy to google if you don't know what you're looking for, but this seems like a reasonable summary: https://plato.stanford.edu/entries/frege-logic https://plato.stanford.edu/entries/frege-logic You can see that the turnstile symbol |- was already used, and the horizontal line (which was called "Fregescher Schlussstrich", Frege's Conclusion Stroke) in my class, was apparently somehow part of the turnstile itself and only became a separated element in modern notation it seems.
- cubefox 3y ago"Schlussstrich" is probably more "deduction stroke" or "inference stroke".
- guerrilla 3y agoSometimes I just hate it when somone gives away my hard-earned arcane knowledge for free ;) I sure wish this post existed when I learned this stuff. I hope increased accessibility leads to less shit languages though.
- otikik 3y agoAmazing answer, starting from fundamentals and evolving from there.
- max_ 3y agoI didn't know there was a language dev Stack Exchange. This is such a pleasant discovery for me.
- layer8 3y agoDespite a CS major, I still get confused about the meaning of |– vs. |=, and about the respective meta-syntactic levels of the variables used. Ironically, one issue for me is the lack of explicit typing in the notation itself.
- peanutcrisis 3y agohttps://philosophy.stackexchange.com/questions/10785/semantic-vs-syntactic-consequence https://philosophy.stackexchange.com/questions/10785/semanti...
- layer8 3y agoThis reminds me that the “model” terminology also confuses me. A “model of X” for me is an idealized and simplified/abstracted version of X, whereas in mathematical logic it seems to be the opposite, a concretization/instantiation.