hlinting agda

[jrp2014]

At present, the master code triggers just shy of a century of different types on hunting suggestions:

Move brackets to avoid $
Use curry
Use list comprehension
Use :
Redundant $
Use guards
Use <=<
Use lambda-case
Replace case with maybe
Use const
Redundant bracket
Use newtype instead of data
Use void
Use list literal pattern
Redundant do
Use fmap
Use concatMap
Reduce duplication
Use zipWith
Use mapMaybe
Use infix
Use unwords
Redundant return
Avoid lambda
Use elemIndex
Eta reduce
Fuse mapM/map
Use first
Use foldr
Use camelCase
Use lambda
Use if
Redundant if
Use /=
Use break
Redundant guard
Use let
Use and
Use gets
Fuse concatMap/map
Use String
Use record patterns
Use replicate
Redundant variable capture
Use section
Move map inside list comprehension
Use elem
Use tuple-section
Use any
Use intercalate
Replace case with fromMaybe
Use print
Fuse mapM_/map
Use maybe
Use >
Redundant lambda
Use <$>
Use =<<
Functor law
Fuse foldr/map
Use catMaybes
Use map once
Avoid lambda using `infix`
Hoist not
Use unless
Use zipWithM
Use &&
Fuse mapMaybe/map
Unused LANGUAGE pragma
Use second
Use <$
Redundant flip
Use id
Use list literal
Use notElem
Parse error
Use negate
Redundant ==
Redundant list comprehension
Use fewer imports
Use maximum
Use forM_
Redundant id
Monad law, left identity
Use $>
Use ||
Use isNothing
Use uncurry
Use asks
Use <|>
Use .
Use null
Use forM
Use typeRep
Use ++
Use all
Use find

Many of these are purely syntactic (eg, redundant brackets, redundant do, redundant $, etc).
Some of them might improve readability (\ _ -> fn could be const fn, etc).
Others suggest the use of more idiomatic style (Use null, maximum, intercalate, maybe, print, etc)
Others still suggest the use of simpler forms (eg, by fusion) or could well result in some performance improvements.

Now, it may be that people have strayed from hlint's suggestions because they used an older compiler or the thought that the current code is easier to read or it was machine generated. I'd be happy to have a go at some of the lower-hanging fruit, but thought it might be worth asking here why it might not have already been done. (The hacking guide is not specific enough to answer some of these questions and there is no hint.yaml file to suggest which hints should be ignored.

[jrp2014]

... and here are some examples:

src/full/Agda/Main.hs:178:10: Warning: Use void
Found:
  fmap $ const ()
Perhaps:
  Control.Monad.void

src/full/Agda/TypeChecking/RecordPatterns.hs:62:30: Warning: Use id
Found:
  \ x -> x
Perhaps:
  id

src/full/Agda/TypeChecking/Telescope.hs:537:15: Warning: Redundant flip
Found:
  flip
    find
    boundary
    (\case
       (Var i [], _) -> i == x
       _ -> __IMPOSSIBLE__)
Perhaps:
  find
    (\case
       (Var i [], _) -> i == x
       _ -> __IMPOSSIBLE__)
    boundary

src/agda-licences/Main.hs:140:6: Suggestion: Use <=<
Found:
  \ f -> putStr . unlines . lines =<< readFile f
Perhaps:
  (putStr . unlines . lines) <=< readFile

src/full/Agda/Auto/Convert.hs:140:20: Warning: Fuse mapM/map
Found:
  mapM (\ name -> getConst False name TMAll) (map I.unDom fields)
Perhaps:
  mapM ((\ name -> getConst False name TMAll) . I.unDom) fields

src/full/Agda/Auto/NarrowingSearch.hs:613:1: Suggestion: Use guards
Found:
  choosePrioMeta flip pm1@(PrioMeta p1 _) pm2@(PrioMeta p2 _)
    = if p1 > p2 then
          pm1
      else
          if p2 > p1 then pm2 else if flip then pm2 else pm1
Perhaps:
  choosePrioMeta flip pm1@(PrioMeta p1 _) pm2@(PrioMeta p2 _)
    | p1 > p2 = pm1
    | p2 > p1 = pm2
    | flip = pm2
    | otherwise = pm1

src/full/Agda/Compiler/MAlonzo/Compiler.hs:279:9: Warning: Redundant variable capture
Found:
  _ <- sequence_ [primNil, primCons]
Perhaps:
  sequence_ [primNil, primCons]

src/full/Agda/TypeChecking/Level/Solve.hs:58:25: Warning: Monad law, left identity
Found:
  return xs >>= filterM (\ m -> isNothing <$> isInteractionMeta m)
Perhaps:
  filterM (\ m -> isNothing <$> isInteractionMeta m) xs

src/full/Agda/TypeChecking/Rewriting/Confluence.hs:633:19: Warning: Use asks
Found:
  ($ x) <$> ask
Perhaps:
  asks ($ x)

src/full/Agda/TypeChecking/Monad/Options.hs:231:16: Warning: Functor law
Found:
  isJust <$> optInputFile <$> commandLineOptions
Perhaps:
  isJust . optInputFile <$> commandLineOptions

src/full/Agda/TypeChecking/Patterns/Abstract.hs:41:16: Suggestion: Fuse foldr/map
Found:
  foldr (A.AsP info) p' (map A.mkBindName xs)
Perhaps:
  foldr (A.AsP info . A.mkBindName) p' xs

src/full/Agda/TypeChecking/Serialise/Base.hs:396:68: Suggestion: Use <=<
Found:
  \ args -> icodeNode =<< icodeArgs (Proxy :: Proxy t) args
Perhaps:
  (icodeNode Control.Monad.<=< icodeArgs (Proxy :: Proxy t))

If some of this code is machine-generated, then it would probably be better to fix the generator and reduce some of the common cases. Eg, pre-pending an element of a list using ++ is expensive, relative to :. Traversing lists multiple times with maps that could be single pass, if fused, should surely be addressed.

[andreasabel]

I'd be a bit careful with hlint and its suggestions. (I remember Johannes Waldmann telling me he originally implemented hlint because he was tired to give the same feedback over and over again to his Haskell students.)

We should of course agree on a style, but it need not necessarily be the one of hlint. FYI: there is a style guide adapted from Tibbe's here: https://github.com/andreasabel/haskell-style-guide/
But even this style is not consistently implemented, and it is not meant to be a hard guideline, rather a soft one.

Many of these are purely syntactic (eg, redundant brackets, redundant do, redundant $, etc).

Indeed, and not all of hlint's suggestions are improvements. Take redundant do: I find it quite useful to have redundant dos in a lot of places. e.g.

f lots o arguments = do
   a single long line

The do is redundant, but it serves a purpose: One can now simply add a new line to f without touching the other lines:

f lots o arguments = do
   a single long line
   now a second line

Not having to change other lines is good for minimal intrusion into the code, and keeping information delivered by git blame succinct. Also, I often forgot to insert a do where there was no redundant do in the first place, and then I had to start the compiler another time. Each failed compilation attempt is a diminishing of productivity, given the excessive compilation boot times we are facing with GHC and cabal.

Similar, redundant $ can be useful to streamline code appearance, like in

   case foo of
       Aleph -> return $ f x
       Beta  -> return $ g x h iow sfll
       Gamma -> return $ x
       Delta -> return $ foo bar

There is a redundant $ to improve uniformity of code appearance, but hlint isn't clever enough to see the purpose. hlint is just a mindless mechanism.

I'd rather not be bullied by mindless mechanisms. Taking suggestions, yes, but having to obey, no.

... and here are some examples:

I think these examples should be viewed in their context. Some of hlint's suggestions are good, we can use them to improve the code. Some are bad, these need to be ignored. And many would not matter, I suppose.

[jrp2014]

I agree with much of what you say, although the recommended way of using hlint is to generate a .hlint.yaml file based on your code that switches off all the diagnostics (hlint —default src > .hlint.yaml) and then switch on only those that are of interest. So I don’t recognise the threat of bullying. The question in this case is which those diagnostics are?!

I also like to format my code uniformly using stylish-haskell, brittany, ormolu, etc. Again these are not always perfect, but they obviate the need to fuss with formatting while you are trying to get the substance right.

[nad]

We should of course agree on a style

Why? We don't all use the same style, and I don't see this as a problem.

[jrp2014]

My straightforward question is which of the hlint hints is it safe to implement, and which would people prefer to ignore? (If the answer is “all of them”, I’ll let sleeping dogs lie.)

[andreasabel]

Searching for the hint list, I found https://github.com/ndmitchell/hlint/blob/master/data/hlint.yaml or is there some better source?

I once tried hlint with the refactor option on Agda, which would have allowed to interactively apply some of the suggestions, but the refactoring tool was not up to the Agda source code (with CPP statements and the like). Not sure what the capacities of that tool are now.

[jrp2014]

The list above comprises all the hints that occur in the current src directory. I wouldn't try the apply-refact package. Sometimes it works, sometimes not (which is why I'd like to test what people would find helpful before rolling up my sleeves).

[andreasabel]

How to get hlinting started? I think a good way is to compose a list of uncontroversial hints, like e.g. Use /= and add hooks that run hlint with these uncontroversial ones.
The problem is how to organize to process to arrive at the list of hints generally accepted by the developers.
A possible but long-winded process is to:

1. First add all the hints that the Agda code base follows already.
2. Then, per hint issue a PR that implements this hint on the Agda codebase. Developers can then voice their opinion on whether this is a reasonable hint.
3. Item 2. should probably be sped up by just have one PR per group of similar hints.

Or: join the Agda meeting and then this can be done interactively.

As a higher-hanging fruit: implement feature kowainik/hintman#57 to get the hint-man use our own hint list.

[jrp2014]

I don't think that it is worth making an industry out of this task. I don't think that we want 100 PRs to accomplish this task.

To me,

1. there are a few of hints that look like straight improvements (eg, Functor law
   Fuse foldr/map, Fuse mapM/map, Fuse mapMaybe/map, redundant flip).

2. most, if not all, the "use a well-known standard function that does the same thing" (const, id, concatMap, ...) see like no-brainers to me too

3. then there are there are some cases which are more matters of taste / style (redundant do, Use $>, Use ||, Use uncurry, Use asks, Use <|>, Use ., use section, redundant brackets, etc)

I would argue that the first two categories are worth doing without much fuss (JDI). The third should either be reserved to a trusted member of the community that is willing to put in the time, on condition that everyone else agrees not to bike shed / quibble.

But there are a lot of these potential changes across lots of files, and I would not trust apply-refact to get it right, so it requires some clear time and concentration to carry out what should be a mindless manual task once the right hlint settings have been applied (since hlint comes up with the refactoring suggestion). So it's not something that I'd want to embark on if it's going to create more angst than it solves.

[UlfNorell]

Fuse foldr/map, Fuse mapM/map, Fuse mapMaybe/map

This doesn't always improve readability in my opinion (depends on the involved functions), and I believe GHC can do the fusion itself (no?), so performance shouldn't be an issue.

[L-TChen]

In terms of lower-hanging fruit, there are a number of cyclic imports (*.hs-boot), and it will be nice to get rid of them.

[jrp2014]

Fuse foldr/map, Fuse mapM/map, Fuse mapMaybe/map

This doesn't always improve readability in my opinion (depends on the involved functions), and I believe GHC can do the fusion itself (no?), so performance shouldn't be an issue.

I suspect that ghc does a good deal of fusing, but probably not in all cases, and Agda doesn't build with -O2. Readability is subjective, but nested maps and foldrs are harder for me.

[andreasabel]

Fuse foldr/map, Fuse mapM/map, Fuse mapMaybe/map

This doesn't always improve readability in my opinion (depends on the involved functions), and I believe GHC can do the fusion itself (no?), so performance shouldn't be an issue.

A (stupid) example where the unfused version is more readable is:

foldr (*) 1 . map (+1)

which is clearly the multiplication of numbers after increasing them by one. The fused version

foldr (\ x y -> (x+1) * y) 1

takes longer to comprehend, because one has to understand the anonymous function involved, convince oneself that the +1 is applied to the correct argument. Then there is the nested parentheses one has to parse correctly...

[WolframKahl]

With some practice.

foldr ((*) . succ) 1

can become as readable as the original version...

[andreasabel]

(*) . succ

After 17 years of Haskell, I still have to think what this means, and sort out which argument of * is increased by succ... :-)

[WolframKahl]

That's why I mentioned practice — I am doing this kind of thing a lot...

[andreasabel]

@jrp2014 commented:

I suspect that ghc does a good deal of fusing, but probably not in all cases, and Agda doesn't build with -O2.

Fusion rules are included in -O, which is the same as -O1 and the cabal default optimization level.
See: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/flags.html#optimisation-levels

-fenable-rewrite-rules | Switch on all rewrite rules (including rules generated by automatic specialisation of overloaded functions). Implied by -O.

[jrp2014]

Thanks for looking through #4448 Andreas.

Working through that, and through the next tranche of candidates leads me to observe:

• What is grokable and what is impenetrable depend almost entirely on pattern recognition. If you're not used to turning things into a folds, then it will seem harder to read, but if you are, then having something expressed as a higher-order pattern makes it easier to ingest.
• The code base reflects the fact that it is the product of several hands, each with their own idiosyncrasies: some like multi-way ifs, others prefer case true/false to if, some prefer f x =, others f = \ x, some prefer [x], others x : [], some prefer x <- fun ; return x, others just fun; some prefer all . not, others not.any, and so it goes
• there are some oddities that I haven't figured, like id $ case ... in a do block and single-case case statements. Perhaps this is a laziness thing, but there are no comments to explain.
• The most varied cases involve () and $. I'd be inclined to strip out redundant (), but others find them helpful. There are a lot of cases where I think it is easier to see how many args the top-level function takes if you do f (a+b) (c+d), rather than f (a+b) $ c+d

But my opinions are just that, not least since I haven't invested sweat in getting this project to its current state. Nevertheless, I do think that there is value in using a common set of idioms and, ideally a common layout format, both supported by automated tools. This is clearly not a new thought (not least because someone has configured a bot to hlint the PRs and the Makefile has an hlint entry). For formatting I use brittany / stylish-haskell / ormolu. None of these tools do a perfect job, but having at least local machine-supported uniformity must be a benefit.

This comes back to which of the various hlint-guided idioms is worth scrubbing in? In my case, I prefer the most succinct code rendering (ie, dropping $ and () where they are not needed) as I think that that tends to be easiest to interpret in the long-run. I know that others like to rely on the visual layout of the code. (Much of the code would not be understandable by a new Haskell programmer no matter what you did, because it is lengthy.) We also need to think about the risk of making the code base harder to work with: changing the cosmetics can make it harder to bisect the case of future errors.

[rwe]

Hi, I came across this issue from searching around, and probably ought to have found it earlier.

I recently implemented #4802 (Add minimal hlint.yaml + GitHub workflow) because I had a >1yr old local branch with various hlint fixes that had grown stale, and I was interested in learning more about GitHub Actions.

It looks like this issue had good discussion but was closed without reaching a conclusion. The tack I took in that PR seems to be in line here, which was to include an .hlint.yaml with all warnings disabled, and then progressively enable a few of them (just the low-hanging fruit, and if any are controversial I'm happy to drop them).

Since there was no resolution here I'll go ahead and re-open this issue and link it to that PR to for context.