ірина
lrlna@toot.cafe
does anyone know of a cheatsheet for type system notation in academic papers?
4
0
0
what is the semantic meaning between the ten different brackets (ok a bit of an over exaggeration, but there are at least 4 in this paper), what does the double colon :: mean etc
2
0
0
@lrlna what paper are you referring to?
1
0
0
@lrlna I don’t think I have seen :: outside of the context of x ::= y where it means x can be y.
In general I think the consensus of meanings of different things in this field is not that great, but I think many follow the syntax set up in “The Formal Semantics of Programming Languages” by Glynn Winskel, and then adds what they think they need to it.
1
0
1
medium rare bird
migratory@jorts.horse@lrlna [] is usually substitution but can also be array indexing; ⟦⟧ is usually some kind of semantic/denotational mapping, {} is generally set notation
https://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf is one of the better histories/summaries of what it calls "CS metanotation"
1
1
0
medium rare bird
migratory@jorts.horse@lrlna and https://semanticsarchive.net/Archive/TE0Y2RkN/denotation_brackets.pdf is an interesting note on just the history of ⟦⟧ notation
1
1
0
@migratory "Strachey brackets"!! i would have never figure out how to google that. super useful, tysm for both of these!
0
0
0
@martinbonnin a pretty general call out - i find that any paper i read about a particular language or type system implementation and i don't quite understand the formulas
0
0
0
Harold Carr
haroldcarr@functional.cafe@lrlna also, Guy Steele's paper on notation: https://dl.acm.org/doi/abs/10.1145/3155284.3018773
2
0
0
Thomas Depierre
Di4na@hachyderm.io@haroldcarr @lrlna Oh he had done a paper not only a talk. Thanks so much for making me discover it :)
0
0
0
@haroldcarr oh nice! Someone linked to their slides for this paper. Finding it useful already
0
0
0
@lrlna The best way I know to learn it (which is not ideal, but it's how I did it) is to take a seminar course where you read a bunch of papers and then be lost for half a semester until one day everything just clicks. It doesn't help though that every paper makes up their own subtly different notation.
2
0
0
@lrlna One thing I remember taking me a long time to learn was that the horizontal bar in inference rules is sort of an if-then. It means either "if the things on top of the line are true then you can conclude the thing on the bottom" or "in order to show the thing on the bottom you need to show all the things on top of the line."
1
0
0
@lrlna Square brackets are usually some kind of substitution. Like e[v/x] means "take e but replace all the xs with v." I always forget the order, but I think of it kind of like division, like you divide by x to get rid of the xs and multiply by v to put the vs in where the xs were. Semanticists would probably cringe to hear me say that though.
0
0
0
@theincredibleholk being able to take a seminar course sounds super dreamy right now! But I hear you - you kind of end up learning with practice
0
0
0