News for hackers. Stuff that matters.

A comment on Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains.

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by pmontra on Wednesday August 07, 2019 @02:58AM (#20632512)
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?

[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Shoue on Wednesday August 07, 2019 @08:41AM (#20634130)
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)`.
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by CaptainBern on Wednesday August 07, 2019 @03:09AM (#20632556)
> 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.

[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by HerrMonnezza on Wednesday August 07, 2019 @03:17AM (#20632587)
3) Backslash before keywords looks inspired by TeX to me.
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by js8 on Wednesday August 07, 2019 @05:09AM (#20633052)
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.

[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Sharlin on Wednesday August 07, 2019 @06:25AM (#20633403)
You mean, modern English keyboard layouts! Square brackets require alt(gr) on my keyboard. Seriously, most European layouts are ridiculously coding-unfriendly.
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by pmontra on Wednesday August 07, 2019 @07:22AM (#20633689)
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.

[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by cinnamonheart on Wednesday August 07, 2019 @01:34PM (#20636920)
Racket does allow usage of brackets and parentheses interchangeably, as far as I know:

    > [define [plus i j] [+ i j]]
    > [plus 1 2]
    3
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by chenglou on Wednesday August 07, 2019 @04:16AM (#20632833)
1) That's a pattern match. Nothing to do with pipe
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by raverbashing on Wednesday August 07, 2019 @04:42AM (#20632938)
"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.
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by bvrmn on Wednesday August 07, 2019 @05:12AM (#20633058)
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.
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by JadeNB on Wednesday August 07, 2019 @05:15AM (#20633073)
> 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'?

[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by pmontra on Wednesday August 07, 2019 @07:25AM (#20633696)
https://www.thefreedictionary.com/backlash

Not so immediate, I admit.

[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by _jn on Wednesday August 07, 2019 @03:07AM (#20632549)
2): Haskell.
[ Parent | on HN ]