[HN Gopher] How should I read type system notation?
___________________________________________________________________
How should I read type system notation?
Author : mpweiher
Score : 95 points
Date : 2023-08-15 20:15 UTC (2 hours ago)
(HTM) web link (langdev.stackexchange.com)
(TXT) w3m dump (langdev.stackexchange.com)
| lcnPylGDnU4H9OF wrote:
| Where could one find an example of this notation "in the wild"?
| UncleMeat wrote:
| Proceedings in POPL or PLDI will have plenty of papers with
| this stuff.
| nicechianti wrote:
| [dead]
| the_af wrote:
| 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.
| agalunar wrote:
| This 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 every 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 euaggelion _good
| news_ = eu- _good_ + aggelos _messenger_ , the double gamma
| pronounced even in ancient Greek as "NGg" ("ng") rather than ":g"
| ("g").
|
| [2]
| https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...
| dvdkon wrote:
| > 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).
|
| What Maths precedent are you refering to? The thing I would
| consider most similar to today's type annotations are
| statements like "x [?] R" or "let x be a set of integers". Im
| both cases the variable comes first.
|
| Besides, it's much more practical this way. An identifier is
| very simple to parse and usually short, while types can be long
| monsters.
| agalunar wrote:
| To clarify, I'm not arguing for "X x" over "x : X", I'm
| arguing for "x : X" over "x: X".
|
| If you _had_ to write it in the form "a: b", however, "X: x"
| would make as much or more sense to me as "x: X".
| downvotetruth wrote:
| The type on the right reasoning may follow the line of argument
| that types may be seen as proofs that have a correspondence
| with judgements (Curry Howard) and judgements as deductions (in
| the sense that the type annotation is explicit and could be
| omitted if the type is able to be deduced from usage) are
| consequences, which come after antecedents and thus on the
| right in LTR script. In contrast, a dictionary is a lookup
| table where the keys need to be first as they are scanned and
| the definitional values do not have a uniqueness constraint,
| hierarchy, strict relationship, etc. Semantically they are
| different and given both the colon's meaning is overloaded and
| context dependent.
| weinzierl wrote:
| That is an interesting view. What you said about the extra
| mental step is true for me when I read the common "X x"
| notation, which is astonishing because I saw it vastly more
| often than "x: X". The later reads very naturally for me and I
| suspect that at least for my brain it is close to how the colon
| is used in natural language. Often you have a proposition and
| what follows after the colon adds detail to proposition or
| describes it in more detail - exactly like a type is additional
| information about the thing to its left.
| contravariant wrote:
| You may be operating under several misconceptions. Firstly the
| notation f: X->Y, putting more space to the right of the colon
| does occur in mathematical writing (admittedly only 1 of the 3
| books I checked used that notation exclusively). Secondly that
| is still a labelling, you're labelling a map of a specific form
| (it's almost never used to label anything else, except when
| dealing with types but that's begging the question).
|
| I suppose it's hard to tell the difference between labelling
| and stating a property, if I had to give an argument I'd say
| that you rarely see a formula on the left hand side, except
| when defining new notations (e.g. let f+g : X -> Y be the map
| defined by (f+g)(x) = f(x) + g(x)). Compare this to something
| like 'let x^2 + y^2 = 1' which kind of functions as a labelling
| (or omits it really) but is really more stating a proposition.
|
| One alternative meaning in mathematics for the colon that does
| truly differ is using ':' as shorthand for 'such that', though
| sometimes people use a . or no symbol at all. This is commonly
| used when defining a set by some proposition e.g. { x : x \in
| IN and x | 2}, but also sometimes when using quantifiers.
| dvt wrote:
| Pretty 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
| agalunar wrote:
| Ah, I should've been more explicit that I was referring to
| programming language syntax. For example, this is
| unfortunately not the convention in Python, Rust, Swift, or
| TypeScript.
| dvt wrote:
| Ah gotcha, I actually 100% agree here. I think both the
| parser (and my brain) would probably be better served by
| space on both sides of a variable : type (or type :
| variable) declaration.
| sophacles wrote:
| The x: X thing maps to:
|
| >Colon used before a description
|
| > Bertha is so desperate that she'll date anyone, even William:
| he's uglier than a squashed toad on the highway, and that's on
| his good days.
|
| As in:
|
| varible x: Its an X.
|
| (edit: formatting)
| agalunar wrote:
| That doesn't match my experience with the usage of a labeling
| or prefatory colon (continuing with my ad hoc terminology).
| I'd read it as
|
| Here's an x: X.
|
| - which is nonsensical (the variable x is not the name of the
| type X, nor is X an example of an x; indeed, it's the other
| way round), or as
|
| It's the case that x: more detailed things that explain or
| follow from x are X.
|
| - which is also backward (since a type is a more general
| thing than one of many specific instances of the type), or as
|
| Here's a quick premise x: the main point is X.
|
| - which is wrong because x is more specific or relevant
| (because it's a local variable, whereas X is likely global
| and shows up in many places; indeed, within a particular
| scope many variables may simultaneously have the same type,
| but a name refers unambiguously to a particular variable), or
| as
|
| Label x: thing X.
|
| - which is wrong because x is not a name for X.
| idreyn wrote:
| Lovely. I've wondered about this for years but never knew quite
| how to frame a query to learn more.
| [deleted]
| armchairhacker wrote:
| This is a nice explanation, but why is it written on stack
| exchange and not (also?) https://lexi-lambda.github.io/?
| IshKebab wrote:
| I 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 wrote:
| Also, 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 wrote:
| The 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
| bloppe wrote:
| I, too, hail from myself.
___________________________________________________________________
(page generated 2023-08-15 23:00 UTC)