Skip to content

Comment on F*: A general-purpose proof-oriented programming languageparent

Comments

I'm the opposite: when landing in a programming language site I want to know the user case the authors had in mind, the memory model, the type system, the compilation targets, the data layout, the control structures, and only at the end just check that the syntax is not indentation based.

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

Indentation based is a pain when copy-pasting between contexts with different indentation levels, as you have to fix it up manually, which is error-prone. In languages without it, you can just auto-format. (And even in an editor that doesn't support that, having a second indicator makes it less error-prone to fix manually)

have to fix it up manually

Any editor written or actively maintained in the current century does this automatically for you. (Yes that obviously includes Emacs and Vim).

But that doesn't work if the indentation carries semantic meaning; you can't change the indentation without changing the meaning. Maybe you can correct syntactically-incorrect spacing (e.g. change 3 spaces to 4 spaces), but not much beyond that.

The Vim I use increases the indent of a code block when I ask it to. Just like it places a closing curly brace at the point where I tell it to. I don't see the fundamental difference between these two things.

But you have to ask it to, and by the right amount for every line/sub-block. If you accidentally get one line wrong, it could be a silent bug. In a language without significant indentation, as long as braces are preserved, once you are done moving code around a single autoformat will fix everything including nested blocks. And if you forget a brace, it's an error instead of a silent bug

no, they can't in indentation based languages. changing indentation implies changing the code. A formatter isn't allowed to do that

In gdb? It's a shame gdb picked python

copy-pasting

Underappreciated benefit of side benefit of indentation based languages: no copy-pasta.

No indeed I'm not a fan. I find it brittle and arbitrary for data values especially; that also makes automatic code generation and edition harder, for no good reason. But that's not an important consideration either way.

What is code edition?

What is code edition?

I think rixed means "code editing" (I guess that rixed is simply not a native (L1) or excellent L2 English speaker).

I don't mind indentation based languages. I used to hate them, but they've grown on me after using python, Haskell, Idris, Agda, etc. And I ended up making my own language indentation based (it is similar to Idris).

That said, it is hard-mode:

- You'll have to figure out how to parse it.

- If you want editor support, it's a pain to get tree-sitter to handle it.

- You may not be able to pull off editor operations like "rename" without implementing a pretty printer (a rename might affect indentation).

I think it is helpful for crude error recovery. On parse error, my language will simply skip to the next column 0 token and parse another declaration.

I did not do this (hindsight), but I would recommend arranging the grammar so you only get indented blocks in cases where the previous line ends in a keyword that introduces it. I think python has a trailing `:` every time indentation is introduced, and Elm does this too - in statements like `let` you need a newline after the `let` to get the multi-declaration version. (This addresses the rename issue.)

a rename might affect indentation

I think I need to see an example.

It happens when the indentation is established on the same line as other code, so having a rule that you need a newline to start indentation will avoid the issue. Examples from haskell:

    foo x y = do a <- something
                 pure somethingElse
Renaming `x` to `xxx` would push the indented block in and the subsequent lines would have to be indented too.

Similarly:

    foo x y = let a = something
                  b = anotherThing
              in somethingElse
Elm avoids this by requiring an newline after the `do` and `let` (if the `let` has multiple assignments).

Edit: This was brought to my attention by an Idris style guide that said: "Indent so that alpha conversion always works with a simple search and replace. In general this would mean starting a new line when starting a new level of indentation."

Thanks

For what it's worth, I love the semantics of many indentation based languages (F# for example) but really dislike editing them. Visually scanning is much easier with braces (imo) and it's much easier to navigate braced languages when using a vim-like editor

For somebody unable to empathize with the "braces are easier to scan" part, could yiu explain why?

I find it easy to see if things are on the same indentation. I find it much harder to visually scan for opening and closing braces unless syntax highliting makes them scream at me or they are accompanied by ...indentation.

I suspect this is a "what you are used to" and have trained yourself to look out for over many years of code reading.

I think this falls under "[wanting] to know the user case the authors had in mind"

There is no "user case", it's called use case.

There is no "user case", it's called use case.

Perhaps English is not a native language for zlsa?

indentation based immediately implies no safe copy pasting, and you can't count on a formatter to untangle the havoc pasting some code can wreak

Honestly, I wouldn't worry about this. Indentation never got in the way of Python's success. There are plenty other things to worry about besides this.

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

Isn't it easy to just auto format it?

You mean add indentation to code where it shouldn't matter?

We need auto-unformatting too? Auto formatting that doesn't get added as a git change?

I just find it funny that the auto formatting adds the spacing to a very specific style, but requiring spacing is too much for some, readability is much richer in most Python projects I've opened (I can't think of one where it was terrible) compared to Java and C# projects I've opened due to people in Python following coding style standards more frequently, PEP-8 is king.

Sure but even with no code indentation at all, an auto-formatter can easily indent everything for you because of the braces. If you have poorly indented code in a language like Python, you're on the hook for indenting everything yourself. And as a bonus, the code won't even run until you do.

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

And I love that people love indentation based languages so I show them a file with some spurious tabs to see how they feel about indentation causing silent errors.

Use case. Not “user case”.

You'll be disappointed in F* then.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.