Comment by pmontra | Hacker News Reader

Comment by pmontra | Hacker News Reader

Knowing nothing about Homotopy Type Theory and looking at the language only for the way it looks:

1) Nice to see that the pipe is only a | and not |> like in Elixir. One character is better than two (and a Shift key.)

2) {- comment -} probably comes from another language (which one?) but I'm always surprised by the cleverness of language designers, even when there is no need for it.

3) The backslash before the keywords is a backslash, pun intended. Why is that necessary and why did somebody even think about it? Cleverness fails designers sometimes.

4) I like that this-is-a-valid-identifier. This_is_slower_to_type because of the shift keys. ThisIsNotMuchFaster.

Then I'm also wondering what the language is being used for now. Somebody else asked the same question and got downvoted but it looked like a honest question. Is it still borderline to research and will maybe influence mainstream languages or are we already unknowingly using some program written in Arend on our machines or somebody's else server?

1) those are for pattern matching, or sum-type separators in data definitions. Also if `|` were to mean "pipe", it's actually a downgrade because the direction isn't clear. `|>` and `<|` show that they pass data to the right and left functions respectively. If it were `|` what would be the accompanying operator that passes data in the opposite direction? Unix pipe streams data, but these operators are actually function application, so I wouldn't conflate the two, the latter is a much simpler concept, `a |> f == f(a)` and `f <| a == f(a)`.

> 2) {- comment -} probably comes from another language (which one?) but I'm always surprised by the cleverness of language designers, even when there is no need for it.

Haskell has {- -} style (multiline)comments.

3) Backslash before keywords looks inspired by TeX to me.

I actually kinda like the idea. The concept of (limited set of) "reserved keywords" always annoyed the mathematical purist in me.

On an unrelated note, this-is-a-valid-identifier also in Lisp, but weirdly enough, the parens "( )" require shift. I think Lisp should use "[ ]" as parens because they do not require shift on modern keyboards.

You mean, modern English keyboard layouts! Square brackets require alt(gr) on my keyboard. Seriously, most European layouts are ridiculously coding-unfriendly.

Probably because coding was invented (and most of it still is) on an English keyboard.

I switch the layout of my non English keyboard in all coding windows and my fingers know what to press there.

Racket does allow usage of brackets and parentheses interchangeably, as far as I know:

    > [define [plus i j] [+ i j]]
    > [plus 1 2]
    3

1) That's a pattern match. Nothing to do with pipe

"this-is-a-valid-identifier" isn't because you don't know if this is an algebraic expression or not. Not sure how this language disambiguates, if it's using spaces or some other symbol.

All "cleverness" usually comes from struggle with parser generator. It's too many languages in the wild with weird syntax due to lack of interest/skills in proper parser.

> The backslash before the keywords is a backslash, pun intended.

What is the pun? Or, I guess I mean, what is the meaning of the second occurrence of 'backslash'?

https://www.thefreedictionary.com/backlash

Not so immediate, I admit.

2): Haskell.

Reply on news.ycombinator.com