Please, please don't let this be the top comment on Idris. I really want to hear from people who have experience with it in different regards.
For example, what's the editing experience like compared to e.g. OCaml with emacs/Merlin? Is there anyone in a position to compare 1ML's approach to unifying type/value languages vs using dependent types?
1ML doesn't really unify the type and value languages. First-class modules are syntactic sugar over System F-omega, which means that the elaboration/type-checking phase of 1ML duly splits modules into type and value components, which live in separate worlds.
Personally, I find 1ML's approach more pragmatic, or, at least, easier to digest for most programmers - including Haskell programmers. Dependent types are more powerful, but they aren't free from complications. For instance, unifying the type and value languages willy-nilly can cause trouble if you want your value language to be Turing-complete, because now type-level computation can diverge too! In a language based on System F-omega, type-level computation is guaranteed not to diverge, because its type level is the simply typed lambda calculus. Some use cases might warrant providing more powerful type-level computation facilities (e.g. calculating the shapes of multidimensional matrices), but it isn't clear to me that the full power of a Martin-Loef-style dependent type theory is needed.
Haskell allows the use of brackets and indentation to format code, but nobody uses brackets. Do you find Haskell hard to read? And if so, is it because of the indentation? I bring up Haskell because Idris is very similar to Haskell syntactically.
These are functional languages, and there isn't a lot of code to chunk together with brackets. Functions are often just one line, and it's a bit cumbersome to make functions that require multiple lines. Do you believe brackets add to the readability of a one line function?
There's nothing about braces that ensures visual cues to nested code.
Significant whitespace does precisely that. And eliminates brace placement arguments.
int func()
{
while dosomething()
{
dosomething()
dosomething()
doanotherthing()
}
dosomething()
}
def func():
while dosomething():
dosomething()
dosomething()
doanotherthing()
dosomething()
> There's nothing about braces that ensures visual cues to nested code.
A machine can look at the braces and re-indent the code, so that you don't have to look at the braces. All while you rest assured that the meaning didn't change:
I just popped it into Vim, selected all and hit =:
int func()
{
while dosomething()
{
dosomething()
dosomething()
doanotherthing()
}
dosomething()
}
Some semicolons are expected so things are a little off.
The braces didn't do anything for a human until indentations were added, whether by human or machine. If you lifted those braces out, you'd still know that the intent was (although in C it would be wrong :)
The only thing I miss about braces is being able to jump to the end of a block easily. In python and similar that's a bit harder to do with an editor.
> The braces didn't do anything for a human until indentations were added
Having explicit delimiters (I don't care if it's {}, begin...end, or whatever) provide several benefits that I have often used.
1. (by far the most important) They trivialize the recovery of indentation that has been trashed by a bad/misconfigured/unfamiliar editor or coworker who inserted "\t" characters into the file. Just run indent-region or send the file through indent(1).
2. Moving code is easier. Just kill/yank it to where you want it and let indent-region or whatever re-indent as needed. Without delimiters I have to either re-indent manually or use an editor with a feature that changes a region's indent level. Even with such a feature, I still have to tell the editor "move this two levels deeper". With delimiters, I can leave that work to the editor.
3. The movement advantages you mentioned.
As for the extra work of having to close blocks (including the infamous LISP ")))))" motif), that's what features like electric-pair-mode is for.
Even better, delimiters can convey more information. Color cues have proven to be very effective at conveying important information; syntax highlighting is very popular, even when showing code outside an editor (such as inside a <pre> tag). I find extending these color cues to also show nesting[1] to be almost as useful as basic syntax highlighting. (I'm using rainbow-delimiters[2] in that screenshot).
I've never used a language where space indentation was used over curly brackets. So question for those who have... When doing so, wouldn't copying and pasting code around potentially cause a lot of accidental issues? Are there some negatives and side effects of the indentation style? Just curious.
If you copy and paste code irrespective of bracket position, you will have the same problems. It turns out not to be an issue.
A big positive of using indentation is that it enforces a visual indication of scope vs. languages where culturally it is normal to find code with lots of giant one-liners and braces on one line.
But overall, you just get used to it and don't notice it. Everyone who yells about languages that use indentation is bikeshedding in the worst way.
I think it depends on the way your brain works. Some people prefer tables full of numbers, other prefer data visualizations. Some people prefer compact, tight code with lots of symbols. Others prefer spatially organized code. While there are probably people on the extremes and people in the middle. My observations have found lots of people generally fall into two main camps. A number/symbol/dense data aesthetic group, and a visual/spatial group. Left-Right brain? I don't know. Neither is better or worse. It just depends on who you are and who you are working with.
For example, what's the editing experience like compared to e.g. OCaml with emacs/Merlin? Is there anyone in a position to compare 1ML's approach to unifying type/value languages vs using dependent types?