10 ms·

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.

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 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 ago
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 https://dvt.name/logic/horse2.pdf
- agalunar 3y ago
  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 3y ago
    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.
    - chrisweekly 3y ago
      For my part, while I have some mixed feelings about introducing whitespace signifigance, I sympathize w the OP and in TypeScript projects, have sometimes wished for more intuitive disambiguation. As for conventions, I might prefer key: value (trailing space for eg JS props), vs foo :type (leading space for types)
      - EarthLaunch 3y ago
        I try to do this at home [eg 0] and it flabbergasted some coworkers when one such notation accidentally slipped into a day job PR last year. I didn't try to argue for it- but I like it personally, mainly for making control flow easier to skim. 0: https://github.com/Suncapped/babs/blob/prod/src/shared/SharedZone.ts https://github.com/Suncapped/babs/blob/prod/src/shared/Share...
sophacles 3y ago
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 3y ago
  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 type X is not an example of the instance 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 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.
  - sophacles 3y ago
    You are telling the compiler: Set aside a chunk of memory x. Use the details you call X for operations with it. The computer itself doesn't know anything about types or anything else - its just some detail for the compiler to use while generating instructions. A type isn't a thing - it's not an object. It's just a set of constraints that detail valid and invalid uses for the variable.
    - agalunar 3y ago
      We may simply differ here – for me, types are as real as objects. Or, perhaps more accurately, types are as illusory as objects ^_^
  - teo_zero 3y ago
    I always read the colon as separating a term (introduced for the first time) and its definition. Just compare the characters list in literature: Hercule Poirot: an investigator Linnet Doyle: a rich heiress ... with the list of variables at the beginning of a function: x: TypeX y: TypeY It makes perfect sense to me.
deleted 3y ago
[deleted]
weinzierl 3y ago
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 3y ago
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.
- kian 3y ago
  I think f: X->Y could be fairly thought of as labeling the function X->Y with f.
  - yakubin 3y ago
    X->Y is not a function. f is.
    - kian 3y ago
      label the function going from X->Y would be how I was intending that to be read. I'm well aware that X->Y is a type signature ;)
  - OJFord 3y ago
    f: X->Y means f maps an input from domain X (set of all real numbers, say) to output range Y (set of all positive real numbers, say, f could be 'abs'). I think you might be thinking it's LX.Y (L for lambda)? But consider X=Y, LX.X is the identity function, some f: X->X could be the identity function, but it could also be anything else that returns a value of the same type as its argument - it could be 'add1' in this example of X being the reals, for example.
dvdkon 3y ago
> 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 ∈ ℝ" or "let x be a set of integers". In 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 3y ago
  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".
  - rocqua 3y ago
    Putting the type first would be weird in languages that do type inference. Because there you sometimes leave out the type info, but need to add it occasionally. Then it makes sense to append it, rather than pre-pend.
resonious 3y ago
I think "age: int" can be easily converted to English along the lines of "person's age: an integer". So the colon never bothered be too much.
dan-robertson 3y ago
I had assumed ocaml had the space because you put spaces on both sides of the colon in French. I don’t particularly disagree with you but one thing I think about is the symmetry of a relation or operator as written and if it’s meaning. Eg I prefer an assignment operator to not have a vertical line of symmetry. The other operator examples you give like < or + or = take the same type on both sides. : doesn’t even take the same kind on each side (lbs being a value and rhs a type). Maybe it should be written in an asymmetric way because of this.
stefncb 3y ago
Interestingly, the labeling colon is written with spaces on both sides in French.

dvt 3y ago

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 https://dvt.name/logic/horse2.pdf

agalunar 3y ago
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 3y ago
  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.
  - chrisweekly 3y ago
    For my part, while I have some mixed feelings about introducing whitespace signifigance, I sympathize w the OP and in TypeScript projects, have sometimes wished for more intuitive disambiguation. As for conventions, I might prefer key: value (trailing space for eg JS props), vs foo :type (leading space for types)
    - EarthLaunch 3y ago
      I try to do this at home [eg 0] and it flabbergasted some coworkers when one such notation accidentally slipped into a day job PR last year. I didn't try to argue for it- but I like it personally, mainly for making control flow easier to skim. 0: https://github.com/Suncapped/babs/blob/prod/src/shared/SharedZone.ts https://github.com/Suncapped/babs/blob/prod/src/shared/Share...

sophacles 3y ago

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 3y ago
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 type X is not an example of the instance 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 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.
- sophacles 3y ago
  You are telling the compiler: Set aside a chunk of memory x. Use the details you call X for operations with it. The computer itself doesn't know anything about types or anything else - its just some detail for the compiler to use while generating instructions. A type isn't a thing - it's not an object. It's just a set of constraints that detail valid and invalid uses for the variable.
  - agalunar 3y ago
    We may simply differ here – for me, types are as real as objects. Or, perhaps more accurately, types are as illusory as objects ^_^
- teo_zero 3y ago
  I always read the colon as separating a term (introduced for the first time) and its definition. Just compare the characters list in literature: Hercule Poirot: an investigator Linnet Doyle: a rich heiress ... with the list of variables at the beginning of a function: x: TypeX y: TypeY It makes perfect sense to me.

deleted 3y ago

[deleted]

weinzierl 3y ago

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

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.

kian 3y ago
I think f: X->Y could be fairly thought of as labeling the function X->Y with f.
- yakubin 3y ago
  X->Y is not a function. f is.
  - kian 3y ago
    label the function going from X->Y would be how I was intending that to be read. I'm well aware that X->Y is a type signature ;)
- OJFord 3y ago
  f: X->Y means f maps an input from domain X (set of all real numbers, say) to output range Y (set of all positive real numbers, say, f could be 'abs'). I think you might be thinking it's LX.Y (L for lambda)? But consider X=Y, LX.X is the identity function, some f: X->X could be the identity function, but it could also be anything else that returns a value of the same type as its argument - it could be 'add1' in this example of X being the reals, for example.

dvdkon 3y ago

> 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 ∈ ℝ" or "let x be a set of integers". In 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 3y ago
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".
- rocqua 3y ago
  Putting the type first would be weird in languages that do type inference. Because there you sometimes leave out the type info, but need to add it occasionally. Then it makes sense to append it, rather than pre-pend.

resonious 3y ago

I think "age: int" can be easily converted to English along the lines of "person's age: an integer". So the colon never bothered be too much.

dan-robertson 3y ago

I had assumed ocaml had the space because you put spaces on both sides of the colon in French. I don’t particularly disagree with you but one thing I think about is the symmetry of a relation or operator as written and if it’s meaning. Eg I prefer an assignment operator to not have a vertical line of symmetry. The other operator examples you give like < or + or = take the same type on both sides. : doesn’t even take the same kind on each side (lbs being a value and rhs a type). Maybe it should be written in an asymmetric way because of this.

stefncb 3y ago

Interestingly, the labeling colon is written with spaces on both sides in French.