Hacker News Reader

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.

I think f: X->Y could be fairly thought of as labeling the function X->Y with f.

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.

I'm not quite sure why this seems to be so controversial, except for the light abuse of notation in my english. Saying that f: X->Y means f maps an input from domain X to output in range Y is to say that we are defining a function -- and labeling it f, since it could just as easily be labeled g and still be the same function. Defining is naming -- naming is labeling [with scope].

It's not defining a function though, it's describing (by one aspect) a whole class of functions.

Take:

    f: ints -> ints

f can be 'add1', 'identity', 'double', etc.

If you know that, and calling it 'defining a function' is just loose English (you didn't mean completely defining) then fine, but that's what's confusing people.

It read to me like you thought it was equivalent to a function definition in code, X & Y described what would actually happen over different inputs, so I was just trying to explain, didn't mean to offend if you knew already.

Oooh, I see what you're saying. For want of an "s". Yes, in this context, I am aware that it is a whole class of functions -- and that f is a label being affixed to that class of functions. Sorry for the confusion -- that makes much more sense now.

No offense received -- was just genuinely confused as to why it netted two comments and a few downvotes for a seemingly uncontroversial statement. But then again, we're talking mathematical logic here, so loose english is of course reasonably discouraged.

Thanks for the clarification, and I hope you have a great evening!

X->Y is not a function. f is.

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 ;)

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.

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

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.

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.

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)

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/Share...

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)

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.

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.

I think I would completely agree for you if it were a definition and not a type annotation!

That is, "x: 5" instead of "x = 5" (or "x ← 5", &c) looks fine to my eyes. And of course, that's how values for the members of a struct are in fact defined in many languages (such as Rust).

I suppose the underlying point is that has-type is a relation, not a definition. Asymmetrical space around a binary relation violates (my) experience, but it's also a bit confusing to use the same syntax for definition and type annotation.

You may have a broader scenario in mind, but my experience is limited to languages like Rust and C where the type is linked to an object the moment that object is declared for the first time, and can't be changed later. These languages do use the same syntax for definition and type annotation.

I will remember this conversation when I encounter a language that allows this (declaration in the first line, type annotations follow):

  var x
  x : Integer
  x = 5
  ...
  x : String
  x = "hello"

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.

We may simply differ here – for me, types are as real as objects. Or, perhaps more accurately, types are as illusory as objects ^_^

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.

> 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.

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".

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.

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.

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