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

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.