Robust haskell without errors

Question

I'm currently learning Haskell. One of the motivations why I picked this language was to write software with a very high degree of robustness, i.e. functions that is fully defined, mathematically deterministic and never crash or produce errors. I don't mean failure caused by predicates of the system ("system out of memory", "computer on fire" etc), those are not interesting and can simply crash the entire process. I also don't mean errornous behaviour caused by invalid declarations (pi = 4).

Instead I refer to errors caused by erroneous states which I want to remove by making those states unrepresentable and non-compilable (in some functions) via strict static typing. In my mind I called these functions "pure" and figured that the strong type system would allow me to accomplish this. However Haskell does not define "pure" in this way and allow programs to crash via error in any context.

Why is catching an exception non-pure, but throwing an exception is pure?

This is completely acceptable and not strange at all. The disappointing thing however is that Haskell does not appear to provide some functionality to forbid function definitions that could lead to branches using error.

Here's a contrived example why I find this disappointing:

module Main where
import Data.Maybe

data Fruit = Apple | Banana | Orange Int | Peach
    deriving(Show)

readFruit :: String -> Maybe Fruit
readFruit x =
    case x of
         "apple" -> Just Apple
         "banana" -> Just Banana
         "orange" -> Just (Orange 4)
         "peach" -> Just Peach
         _ -> Nothing

showFruit :: Fruit -> String
showFruit Apple = "An apple"
showFruit Banana = "A Banana"
showFruit (Orange x) = show x ++ " oranges"

printFruit :: Maybe Fruit -> String
printFruit x = showFruit $ fromJust x

main :: IO ()
main = do
    line <- getLine
    let fruit = readFruit line
    putStrLn $ printFruit fruit
    main

Let's say that I'm paranoid that the pure functions readFruit and printFruit really doesn't fail due to unhanded states. You could imagine that the code is for launching a rocket full of astronauts which in an absolutely critical routine needs to serialize and unserialize fruit values.

The first danger is naturally that we made a mistake in our pattern matching as this gives us the dreaded erroneous states that can't be handled. Thankfully Haskell provides built in ways to prevent those, we simply compile our program with -Wall which includes -fwarn-incomplete-patterns and AHA:

src/Main.hs:17:1: Warning:
    Pattern match(es) are non-exhaustive
    In an equation for ‘showFruit’: Patterns not matched: Peach

We forgot to serialize Peach fruits and showFruit would have thrown an error. That's an easy fix, we simply add:

showFruit Peach = "A peach"

The program now compiles without warnings, danger averted! We launch the rocket but suddenly the program crashes with:

Maybe.fromJust: Nothing

The rocket is doomed and hits the ocean caused by the following faulty line:

printFruit x = showFruit $ fromJust x

Essentially fromJust has a branch where it raises an Error so we didn't even want the program to compile if we tried to use it since printFruit absolutely had to be "super" pure. We could have fixed that for example by replacing the line with:

printFruit x = maybe "Unknown fruit!" (\y -> showFruit y) x

I find it strange that Haskell decides to implement strict typing and incomplete pattern detection, all in the nobel pursuit of preventing invalid states from being representable but falls just in front of the finish line by not giving programmers a way to detect branches to error when they are not allowed. In a sense this makes Haskell less robust then Java which forces you to declare the exceptions your functions are allowed to raise.

The most trivial way to implement this would be to simply undefined error in some way, locally for a function and any function used by its equation via some form of associated declaration. However this does not appear to be possible.

The wiki page about errors vs exceptions mentions an extension called "Extended Static Checking" for this purpose via contracts but it just leads to a broken link.

It basically boils down to: How do I get the program above to not compile because it uses fromJust? All ideas, suggestions and solutions are welcome.

Answer 1

Haskell allows arbitrary general recursion, so it's not as though all Haskell programs would necessarily be total, if only error in its various forms were removed. That is, you could just define error a = error a to take care of any case you don't want to handle anyways. A runtime error is just more helpful than an infinite loop.

You should not think of error as similar to a garden-variety Java exception. error is an assertion failure representing a programming error, and a function like fromJust which can call error is an assertion. You should not attempt to catch the exception produced by error except in special cases like a server that must continue to run even when the handler for a request encounters a programming error.

Answer 2

Your main complaint is about fromJust, but given it is fundamentally against what your goals are, why are you using it?

Remember that the biggest reason for error is that not everything can be defined in a way that the type system can guarantee, so having a "This can't happen, trust me" makes sense. fromJust comes from this mindset of "sometimes I know better than the compiler". If you don't agree with that mindset don't use it. Alternatively don't abuse it like this example does.

EDIT:

To expand on my point, think of how you would implement what you are asking for (warnings on using partial functions). Where would the warning apply in the following code?

a = fromJust $ Just 1
b = Just 2
c = fromJust $ c
d = fromJust
e = d $ Just 3
f = d b

All of these are statically not partial after all. (Sorry if this next one's syntax is off, it is late)

g x = fromJust x + 1
h x = g x + 1
i = h $ Just 3
j = h $ Nothing
k x y = if x > 0 then fromJust y else x
l = k 1 $ Just 2
m = k (-1) $ Just 3
n = k (-1) $ Nothing

i here is again safe, but j is not. Which method should return the warning? What do we do when some or all of these methods are defined outside of our function. What do you do in the case of k where it is conditionally partial? Should some or all of these functions fail?

By making the compiler make this call you are conflating a lot of complicated problems. Especially when you consider that careful library selection avoids it.

In either case the solution IMO to these kinds of problems is to use a tool after or during compilation to look for problems rather than modifying the compiler. Such a tool can more easily understand "your code" vs "their code" and better determine where best to warn you upon inappropriate use. You could also tune it without having to add a bunch of annotations to your source file to avoid false positives. I don't know a tool offhand or I would suggest one.

Answer 3

The answer was that I wanted was a level of totality checking that Haskell unfortunately does not provide (yet?).

Alternatively I want dependent types (e.g. Idris), or a static verifier (e.g. Liquid Haskell) or syntax lint detection (e.g. hlint).

I'm really looking into Idris now, it seems like an amazing language. Here's a talk by the founder of Idris that I can recommend watching.

Credits for these answers goes to @duplode, @chi, @user3237465 and @luqui.