[spinningslate]

"smacked in the face" might be a bit extreme, but I can sympathise with GP's point. I read the first line of the first example:

    A :: ~ * ~> * => {(list A) :: |new |empty }.

And got stuck at the first hurdle. I started parsing it in my mind and read "A such that tilde star arrow tilde double arrow". I stopped there, and thought "I'm lost". I started trying to interpret it: * might mean wildcard; single arrow could be curried functions (per Haskell). But I don't know what tilde means, nor the double arrow.

Now, of course, I can go and look it up: it'll all be defined somewhere. But that first experience - that very first "I've never seen this before, it sounds interesting" hit a road block right there.

Maybe not smacked in the face, but enough friction for me to click the back button.

[vmladenov]

You can take issue with the order of the presentation but the definition is in the following section. There’s nothing to look up, it’s just an arbitrary choice by the author.

[caotic123]

Yep, these codifications are just examples of what you can do, as Vmladenov said, try reading the examples above.