[ discussion, code style ] Arrows in vertical function signatures

[buzden]

Beware of bikeshedding!

When contributing to pack, I try to preserve existing code style. But there is one thing that makes this annoying and hard for me: it is the placement of arrows at verticalised function signatures. I.e., existing

findInAllParentDirs :  HasIO io
                    => (Body -> Bool)
                    -> Path Abs
                    -> EitherT PackErr io $ List $ File Abs

vs.

findInAllParentDirs : HasIO io =>
                      (Body -> Bool) ->
                      Path Abs ->
                      EitherT PackErr io $ List $ File Abs

For me, arrow belongs to the parameter on the left, because it really-really changes the meaning of it. For me, cognitive load of understanding the latter formatting is sufficiently less. Also, when adding a new parameter to an existing function, again, it's much less work to understand what to do and how to not to mess up what's already there.

So, the question is: @stefan-hoeck is it important to you that the current styling is used, or it is an arbitrary choice (or, maybe, a Haskeller habit) that can be revisited?

[stefan-hoeck]

I think the same style should be used throughout the code base. I have accustomed myself to using the style you see in the code, which is used in all/most of my Idris packages, so I'm afraid I'm not going to change that (unless there are very strong reasons convincing to do otherwise).

[buzden]

I think the same style should be used throughout the code base.

If we are talking about whole pack, it's not a problem to have the same style throughout, see https://github.com/buzden/idris2-pack/commit/6c265bfa2c8c2ed37f53aeca249ce7fe612e2059

so I'm afraid I'm not going to change that.

Okay, that's anyway about personal preference and experience. So, closing, then.

[stefan-hoeck]

Sorry, I probably was too negative in my last comment, especially since I just now realized what the actual difficulty is: We can't see, whether an argument is an auto-implicit without looking at the arrow on the next line. That's indeed something I haven't considered before. Let's do the following: Since everybody likes some decent bikeshedding from time to time, I'll post on the Idris discord asking the community about people's favorite style for lengthy function signatures. If we can agree on a solution, it probably makes sense to adapt to this newly established best practice.

[stefan-hoeck]

I have thought again about this after all the talk on Discord. Here's my suggestion:

module Style

import Data.IORef
import Data.SortedMap

foo :
     HasIO io
  => {auto ref : IORef (SortedMap String Nat)}
  -> String
  -> Nat
  -> io ()

Core ideas:

• Long type signatures should be safe under function renaming : Start them on a new line.
• Prefix each line with an arrow, but use plain arrows except for interfaces, which should be listed at the very beginning of the signature
• Use {auto ...} syntax plus single errors for auto implicits that are not interfaces

@buzden: What do you think?

[buzden]

I'm assuming that you are asking for my personal opinion ;-)

From this discussion on Discord I realised that I'm not alone in the view on the signatures, at least there are several people who think very closely to mine point of view; but at the same time I realised that variety of points of view is much wider than I thought.

Speaking of your suggestion, I (personally!) dislike it and here it why:

• this is not the one I'm familiar with, it is not the one which I used to see in Idris'es codebase, your libraries or any Haskell code; that's why (at least for some time) it will be hard to perceive for me;

• I personally dislike the long space before the first argument; this visually does not look like other indentation-based parts of the language (like do-notation and most common use of series of lets) where equally meaningful things are indented equally; well, your original style technically also does not have this property, but it at least looked visually the same, i.e. like

  blahblahblah
    foofoofoo
    barbarbar
  

• Answering to your

  ...interfaces, which should be listed at the very beginning of the signature

  I must say that there are some situations where interfaces cannot go first, where you should specify something about parameters of interfaces themselves, e.g.

  f : {p : SomeSpecifiedType -> MoreTypes} ->
      SomeInterface p =>
      TheRestOfTheSignature p
  

  However, as far as I know, particularly in pack's codebase there are no such interfaces and functions;

• I personally don't like to write auto-implicit arguments by hand in function signatures, you won't find it almost anywhere in my project's code (except for records, maybe). Despite my personal view that (...) => syntax is clearer than {auto ...} ->, there is one more point. I think that distinction between interfaces and non-interface auto-implicits does not follow the pragmatics of the Idris language. I personally consider things which are not interfaces like IsSucc n and NonEmpty xs and things that definitely are interfaces, like HasIO m, like pragmatically same things which deserve the same syntax, because both of them are needed for the similar thing -- to define a constraint on an argument in the signature. Following your suggestion, I will need to use =>-syntax for HasIO, but {auto ...} -> syntax for IsSucc, which I think weird and requires more cognitive load both to write and to understand. Moreover, refactoring interface to more complicate datatype would require changes in all signatures which use it without much change in the meaning, which I think shouldn't happen (however, I would agree that this situation is rather seldom).

• As I said in Discord, I look and perceive signatures much more often than rename functions, and this is why I think that style of signatures which make them look (subjectively) harder but allowing shorter diff on function renames does not worth it. However, I understand that it may be hard to understand long diff of big commit (or whole PR) when some functions are renamed and some are moved up or down in the file: with you suggestion such diff would be much more comprehensible. I don't have a universal solution for this for a style that has the first argument on the same line as the function name, but I personally try to do renaming and other things in separate commits of pull requests precisely for making code review easier. Moreover, smart diffs like on GitHub show change cleanly when only indentation was changed, which makes review easier.

[stefan-hoeck]

Thanks for the detailed answer. I was asking for your opinion in particular because you started this discussion by opening this issue. I can see your points - they are all valid, but they are also very much a matter of taste and personal preference. The opinions in the discussion on discord varied quite a bit, and I perceived no clear favorite there.

About interfaces going first: I'm aware this is not always possible, so there might be exceptions.

Personally, for me arrows coming last just don't look right and make the line harder to read than aligned arrows at the beginning of the line. At the same time - as was mentioned by other people on discord - using {auto ...} -> instead of the more concise => makes auto-implicits stand out more.

Perhaps one day, we as a community will come up with some best practice and automatic linter. Until such times, I think I'll stick to the style mentioned above. I'll close this for now, as its an opinionated matter, and we are unlikely to come to an agreement here, which is not a bad thing.