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

user_5822450 0
Viewed 126

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.

proof-of-correctness functional-programming haskell
2 Answers

Using fromMaybe (or fromJust) (option 1) is a typical way to "tell Haskell 'just trust me'" (option 4).

What is smelly is precisely having to say "just trust me", because programmers are untrustworthy. Users of strongly typed languages prefer encoding invariants in the type system so they can be enforced automatically. However arithmetic is a notorious aspect of programming that mainstream type systems are not yet well-equipped to handle, so you do have to resort to throwing errors in unreachable cases. Dependent/refinement types (cf. Liquid Haskell) are a technology that would let you reason about arithmetic within a language's type system.

user_68637490

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
user_10485720
Related