What does | solve?

They are also using : ; , and a new line. Also ' and << >> that I have no idea how to type.

They are using both :~ and :: for type hints.

In none of the languages I've seen that was necessary or useful.

I think the problem they were solving was ... we really want to be able to cram everything into one line, so even if you split lines you might just as well still use the same characters despite them being unnecessary then.

The syntax `expr :~ annot` is used to annotate the expression with static information. This is different from type annotations.

It's a general mechanism to associate an expression with "extra information" that can be used elsewhere (at compile time).

One can for example using static information to implement dot notation for an object system. Using static information, one can push name resolution from runtime to compile time.

The important part is that users of Rhombus can use the mechanism for tracking static information specific for their programs.

It will be exciting to see the creative uses of this mechanism in the future.

https://docs.racket-lang.org/rhombus/static-info.html

> The syntax `expr :~ annot` is used to annotate the expression with static information.

Compiler can tell if a thing is static or dynamic and apply the correct behavior. Why would I ever want to check static thing only dynamically and why would I ever want to try statically check dynamic type if not by mistake?

If programmer doesn't really have a real choice why make him choose which buttons to press?

The idea behind macros is so to speak to allow the programmer to extend the compiler.

In a language like MetaPost I can use equations between variables:

   x + y = 10
   x - y =  6

A reference to a variable x will use the current set of equations and solve for x. The solution (it it exists) will become the value of the variable reference.

Let's say I want to extend Rhombus with this new kind of variable (let's call them linear variables).

Each linear variable needs to have some static information attached. Here the relevant information is the set of equations to consider. A reference to a linear variable will then reduce (at compile time) the equations associated with the variable. The reduced set of equations is then used to generate runtime code that finds the value.

In a sense "static information attached to an expression" is just a convenient way of working with compile time information (in the sense currently used by macros in Racket).

Is that the reason for two different type annotation signifiers? That some day I might want to extend the language with something?

It sounds a bit like if every C function (including hello world) had to have empty asm block because someone might need it some day.

The operator `expr :~ annot` simply attaches the static information to the expression.

The operator `expr :: annot` will at runtime insert a check that the expression satisfies the annotation.

What if I want both behaviors at the same time? Have some static information attached and also do a runtime check?

I'm a bit confused: Can this static information system be used for run-of-the-mill static type checking as well or not? And if so, does a static type checker for this language exist or is one in the works?

> Can this static information system be used for run-of-the-mill static type checking as well or not?

Yes.

As an example Matthew Flatt has implemented Shplait in Rhombus:

https://github.com/mflatt/shplait