Handling errors correctly

I know I should avoid both exceptions and partial functions that can throw them.
I also know that I should handle all cases with pattern matching, however by doing so I risk having runtime errors every time I forget a case.

Other options are:

  1. Maybe
  2. Left/Right
  3. avoid error-generating states can be represented with data structures such as NotEmpty Lists.

It is easy to write functions with Maybe, however if the calculation fails I get Nothing and I don’t know where it failed.
I would like to see code examples with correct error handling with Left/Right and using data structures like NonEmpty.
Are there code examples that show proper error handling?

Option 3. (avoiding error-generating states) is what you should be striving for. If you haven’t already, I suggest this famous article: Parse, don’t validate.

It is not always possible to do that, though. In this residual case, an Either MyError a is a good, practical choice.

2 Likes

In Either MyError a, What type should MyError be? String? A new data type?

It really depends on what you call errors (and exceptions)
Exceptions normally refers to problem which happen exceptionnaly (i.e pretty much never), for example disk full, network error etc …
They are normally not part of the normal workflow and most of the times you can’t do anything about it, apart from catching it at the top level and display and exit gracefully.
In that case it’s not really different from not doing anything.

Then there are errors. What do you call an error ?
If you try to lookup a value in a list (or map) and you don’t find it : is it an error (because you know it should be there), or just something which can happen.
The first case might happen because you are looking for the value flag in a list of options and you know that it should be there.
In that case, you probably should change your data structure to something which enforce the presence of this value.
The other case, for example you have a list (or a map) of pair name and their plural form. You are only expecting the irregular plurals to be part of the list so returning Maybe is fine.
Not finding it is not an error and you don’t need to know where it fails because it hasn’t fail.

For example to get the plural of a word you’ll have

plural :: Map String String -> String -> String
plural irregularMap name = fromMaybe (name ++ "s") (lookup name irregularMap)

I use fromMaybe to deal with “error” nothing in irregularMap. There is no error to propagate.

Using either is usually needed when you need to report an error to the user which gave you an invalid input.
This is unavoidable if the input is a for example a text file which needs to be parsed but can be avoid most of the time by a better UI.
If you are not doing user facing application, but for example a script to draw a chart from data in a database you shouldn’t need to know “where it failed”, because nothing should fail (option 1 & 3).

1 Like

If your unhappy paths are finite, you can model errors with a sum type. For example, I have work code that looks like

data ThingValidationFailure = 
  ThingInactive ThingId
  | NestedThingInvalid ThingId NestedThingId
  | BadDate ThingDate
  | InvalidData

This way, I can produce “errors” as values, and this mapping can work across single values or collections equally. With a type like Either ThingValidationFailure Thing, I get short-circuit validation, where I bail out on the first failure and get back a Left containing it. Since my error values can be product types, I can pack in contextual information for consumers of those errors. If I want to accumulate error values, I can use a type like Validation (NonEmpty ThingValidationFailure) Thing to signify that I’ll either get a Success Thing or a Failure (NonEmpty ThingValidationFailure) containing all the error values encountered.

This way, you can model the error domain of each subdomain of your problem cleanly, then map between them as necessary to bubble error states up to wherever they’re relevant or just resolve them where they come up.

2 Likes

My unpopular opinions:

  1. It depends.

  2. Do you truly prefer, e.g., (/) :: Fractional a => a -> a -> Maybe a? Have you actually used it in anger? Does its safety help or does it get into the way? Must partial functions be crimes unconditionally without exceptions?

    Perhaps 50 years from now, when FP people actually use Coq or Lean or refinement types in anger (as opposed to just talking about them, such as now), then we can declare (/) :: (Eq a, Fractional a) => a -> {x::a | x /= 0} -> a, and it is total and safe and convenient, and good and fast and cheap and you can pick more than two.

    For the here and now, I accept a few judiciously chosen partial functions after considering what my use cases actually look like.

    I most appreciate libraries that provide both a partial function and a Maybe function. For example Data.Map[.Strict] has both versions of looking up: (!?) :: Ord k => Map k a -> k -> Maybe a and (!) :: Ord k => Map k a -> k -> a. I have benefitted from both.

  3. Exception is not a crime if the context is IO. IO is where exceptions are safe and unobstrusive.

  4. The Structure of Structured Flow

2 Likes

I think those ‘unpopular opinions’ are more or less the mainstream view? I think ‘parse, don’t validate’ is a great slogan and a great design pattern and I use it when applicable, but I also think it gets so much emphasis in Haskell at least in part because people coming from other languages are so used to doing things the other way that they need some strong words to get them used to the idea.

There’s also a big difference between programming in a library context, where you almost always want your code to be considered rock-solid by your users, and where they expect you to communicate all the ways your functions might fail via their API; and in an application context, where maybe you want the application to be rock-solid but maybe you want it to fall on its face quickly as soon as it encounters something you weren’t expecting to happen (or maybe you don’t much care but you do care a lot about getting the feature shipped by Thursday).

2 Likes

Both Coq and Lean define n / 0 as 0, so that division is total. You don’t even need Liquid Haskell to do that :smiley:

1 Like

It might be a bit involved, but you may find some inspiration in parsing libraries, as it’s fairly typical to want to explain the reason for the failures in context.

For example, aeson - Data.Aeson - has some code around this with modifyFailure and such.

1 Like

This is pretty much my rule, yeah. I write applications as thin, horrific layers over nicely modeled library code. If my library code fails, it emits a value of some kind that a consumer can do something about. If the application I’m writing over that library gets one of those, it nearly always just explodes immediately. :smiley: I think this still aligns with the “parse don’t validate” pattern, since the point is to draw a clear boundary between “business logic” and “untrusted IO”. Ultimately, I think of it as a particular way to implement what other people call “hexagonal architecture” or “ports and adapters”.

1 Like

If you use effect systems or some subset of similar machinery you can do “checked exceptions” pretty ergonomically. Then you can have errors tracked in types but also acting like exceptions where you can choose to handle them or not. I think checked exceptions are fairly unpopular, and they add overhead because whenever writing any function that can “throw” you always have to add the possible constraints to it but I like them, and if using an effect system library it makes you want to write in a monadic/do notation way, so probably not recommended if you’re not a believer.

But as an example you can do something like (I didn’t try this)

hiToNumber ::
  ( Error InvalidError :> es
  , Error ImpossibleError :> es
  ) =>
  Text -> Eff es Integer
hiToNumber text = do
  case text of
    "hi" -> pure 3
    "di" -> throwError InvalidError
    _ -> throwError ImpossibleError

hiOrDiToNumber
  ( Error ImpossibleError :> es
  ) =>
  Text -> Eff es Integer
hiOrDiToNumber text = do
  hiToNumber text
    & runErrorWith (\InvalidError{} -> pure 4)

main :: IO ()
main = do
  let number = hiOrDiToNumber "di"
        & runWithError (\(ImpossibleError msg) -> logError msg >> error msg)
        & runPureEff
  print number

in practice you’ll want a bunch of other error handling functions but it’s kinda cool.

1 Like

Perhaps you’ll just be happier using Epigram instead:

Turing-Completeness Totally Free (2015)

While you’re there, perhaps (n/0) = 0 could be useful in solving:

…alternatively, you could always just implement $DEPENLANG in $DEPENPLANG, for your preferred $DEPENLANG.

1 Like

Both Coq and Lean define n / 0 as 0, so that division is total.

I believe that this is a good example for @Pluto, of the absolute worst way to handle exceptional cases (and now my respect for Coq and Lean has went from positive to negative). The Real Algebra is not a total algebra. I believe the important part, for “Handling errors correctly”, is to capture the exceptional cases as a value or type, that can be properly checked or handled, rather than to plaster over them in an expedient way covering up the errors.

Techniques to resolve these engineering issues in Haskell for Real Numbers are, for instance, with IEEE-754 Floating Point, to have silent and signaling NaN, +/-Inf as a value with functions to check those conditions. Otherwise with an alternative to Floating Point, Posit Numbers, it’s to have Not-A-Real (NaR), with the overall system being isomorphic to Maybe Rational. The Haskell implementation of ‘posit’ has totality checking of the constructors for NaR and R recovering the totality, and GHC will warn if not properly handled.

2 Likes

I know that it is quite shocking when you first hear that this is how proof assistants (basically all of them) handle partial functions. But there is a very good reasoning behind why they do it this way, and it is not because they don’t know about the solution using Maybe/Either types. For example, you can read Kevin Buzzards explanation here: Division by zero in type theory: a FAQ | Xena or Lawrence Paulson’s here: Undefined values, or what do we get when we divide by zero?

But the basic idea is that you don’t want to give up on the very simple syntax of arithmetic expressions, and don’t want to add “error handling” in the middle of some chain of equations or inequations that your mathematical proof is about. It turned out to be much more ergonomic to just handle this with side conditions which state that the respective arguments can never be zero, for example.

3 Likes

…and blithely treating n/0 as being 0 in the tools of the future, used to design the computers of the future, must surely be a bad habit!

You did hedge with ‘basically’, but Agda is a prominent exception.

1 Like

Ah, so my precaution with “basically” paid of :sweat_smile:. I should have checked this first, but I mostly have experience with tactic-based proof assistants. My guess would be that the fact that Agda is less tactic-based and more pattern-matching and functional-programming based changes which solutions are more or less ergonomic. But yes, I have very little experience with the mathematical libraries of Agda.