haskellfunctional-programmingproof-of-correctness

What is the proper solution when using find with a guaranteed value?


In Haskell, find is designed to evaluate as a Maybe, because when scanning a list for an element matching a predicate, it could fail. However, consider the following:

factorize n | isPrime n = [n]
            | otherwise = m : factorize (n `div` m)
            where m = find ((==0) . (n `mod`)) [2..]

find here will clearly find a value in every case, assuming we’re only hitting integers greater than 2. If a number is not prime, then it has a factor somewhere in the infinite list [2..]. But of course, Haskell doesn’t know that, and will still complain that a Maybe is being used. What is the solution here?

  1. Use fromMaybe with some dummy default value to extract the inner value. The default value will never be used.
  2. Use something like head . dropWhile to act as a kind of “unsafe find”.
  3. Bubble the Maybes all the way up and have the factors returned as a list of Maybes.
  4. Some way to tell Haskell “look, the math checks out, this is safe, just trust me.”

1 and 2 are smelly, 3 is cumbersome and adds failure state to a function it shouldn’t exist in, and I don’t know whether 4 exists. What is the best solution here?

Edit: The above list of options is incomplete without mentioning fromJust, which takes a Just and returns the value inside it, and throws an error when given a Nothing. I think that's clearly the short answer to my question, and I wasn't aware of its existence until I read the answers and comments here. However, there are still good points made about safety and fail state in general in the answers below.


Solution

  • Solution 1 would work, but is unidiomatic.

    Solution 2/4 would be to use fromJust or pattern matching:

    factorize n | isPrime n = [n]
                | otherwise = m : factorize (n div m)
                where m = fromJust $ find ((==0) . (n `mod`)) [2..] -- trust me, if a number is not prime, then it has a factor somewhere
    
    factorize n | isPrime n = [n]
                | otherwise = m : factorize (n div m)
                where (Just m) = find ((==0) . (n `mod`)) [2..] -- trust me, if a number is not prime, then it has a factor somewhere
    

    The comment is kinda important to point out to the reader that this is safe and will never cause an exception. There's no way to tell Haskell though, it will still generate code to throw an exception should a Nothing occur.

    You'll need to prove its correctness yourself. You may notice that it's actually wrong - try with factorize 1!

    What is the best solution here?

    Don't duplicate the work in the first place. isPrime will also try to find a factor, then return False if it found one and return True if it didn't. Instead of trying to find the factor again in the case where isPrime n returned False, use the factor from the search you just did!

    -- TODO: prove that the returned factor is actually prime
    -- TODO: optimise by using [2..(floor $ sqrt $ fromIntegral n)]
    findPrimeFactor :: Integer -> Maybe Integer
    findPrimeFactor n = find ((==0) . (n `mod`)) [2..n-1]
    
    factorize 1 = []
    factorize n = case findPrimeFactor n of
                    Nothing -> [n]
                    Just m  -> m : factorize (n div m)
    
    isPrime 1 = False
    isPrime n = case findPrimeFactor n of
                  Nothing -> True
                  Just _  -> False
    

    or alternatively

    -- TODO: prove that the returned number is actually prime
    findPrimeFactor :: Integer -> Maybe Integer
    findPrimeFactor n = find ((==0) . (n `mod`)) [2..n]
    --                                               ^ note the difference
    
    factorize n = case findPrimeFactor n of
                    Nothing -> []
                    Just m  -> m : factorize (n div m)
    
    isPrime n = (Just n) == findPrimeFactor n