Finding and preventing errors in Haskell code

Learn
1

I am a moderately experienced OCaml programmer and I am interested in learning more about Haskell. Specifically I am interested in finding and preventing errors in code.

Famously, the Haskell compiler catches many potential errors at compile time, and if you design your abstract data types well, then you can use the module system to make global guarantees about program correctness (all values of this type throughout the entire program always have a certain property) from local reasoning (the “constructors” for the type guarantee the property, and the privileged functions in the module preserve the property).

Second, you want to write lots of unit tests, and QuickCheck can help with this.

If I want my code to be reliable, what other tools should I be familiar with beyond what’s part of GHC? Does anyone use Semgrep, CodeQL or another general purpose static analysis tool to find errors in code? I have heard of Liquid Haskell, seems cool and I will be checking this out.

4 Likes
2

Nice topic! Of course it depends a bit on the type of code, but here are some ideas/things I do:.

Regular/disciplined/consistent process, code review, cleanup, style and the like - all of these probably help. Code linting (hlint, stan..) and formatting tools (ormolu, fourmolu..) might be useful.

Beyond type-related errors, don’t forget to eliminate partial code - things that compile successfully but can fail at runtime. Linting tools and/or ghc -Wall can help detect some of these. Some examples:

  • use of partial functions in your code (head, !!, maximum, fromJust, error, read etc)
  • use of partial functions in your dependencies
  • printf formatting strings with mismatched arguments
  • assuming that regular expressions generated or received at runtime are well formed
  • working with text without handling decoding, wrong or missing system locale, etc.

For testing (via) console output, I like shelltestrunner.

For testing or at least monitoring performance, I like to log one line of performance measurements (time & memory) frequently to a persistent log, eg each time functional tests are run. Also, quickbench for quick ad-hoc comparisons.

For cross platform testing, github workflows make it relatively easy to test on the big ones.

There’s no substitute for real world testing by many users.

And, anything you can do to speed up the process of finding bugs, fixing, and getting the fixed version into the hands of users increases the perceived reliability (for the users that didn’t hit the bug).
One way to speed up the finding part, other than having many adventurous users, is to incentivise bug reports, eg with bounties.
One way to speed up the fixing part, other than having many responsive developers, is to have optional detailed debug output available.

QuickCheck inspired a whole family of similar tools (hedgehog, smallcheck etc.) - they’re probably all worth checking out. More generally, any kind of fuzz testing, including with external tools, seems useful.

Another important approach is simulation, allowing you to test your system in specific conditions and in accelerated time (like the TigerBeetle people).

LiquidHaskell (as you mentioned) adds powerful contracts, augmenting the Haskell type system.

Generating Haskell code from a language which allows more formal proof (like the Cardano people) is probably another good technique.

4 Likes
3

Most of the suggestions in the previous reply appear to me, while all useful, as not very Haskell-specific. I used think that the OCaml type system is of comparable expressiveness to Haskell, so you would not need to switch languages to gain more static guarantees.
I don’t know OCaml well - do you see anything in @simonmic’s suggestions that OCaml can not offer? Certainly OCaml has excellent linters, ramdomized testing, etc?

2 Likes
4

Yes, I don’t mind that they’re not Haskell specific. I am still curious.

The OCaml compiler gives a lot of useful feedback. OCaml has a similar type system to Haskell, although using higher-kinded types requires a translation/encoding using the module system.

There is an OCaml port of Quickcheck. GitHub - c-cube/qcheck: QuickCheck inspired property-based testing for OCaml.

There are various formal proof languages that transcompile to OCaml. Rocq is well known but you can only really export first-order functions operating on ground types AFAIK. Why3 and F\^ast transcompile to OCaml, Why3 has contracts and F^\ast has refinement types.

There is an emerging standard for contracts/specifications expressed in comments, Gospel, and tools to check the Gospel specifications. I haven’t used many of these things I’m describing.