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

sca*_*ter 3 haskell functional-programming proof-of-correctness

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:

\n
factorize n | isPrime n = [n]\n            | otherwise = m : factorize (n `div` m)\n            where m = find ((==0) . (n `mod`)) [2..]\n
Run Code Online (Sandbox Code Playgroud)\n

find here will clearly find a value in every case, assuming we\xe2\x80\x99re 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\xe2\x80\x99t know that, and will still complain that a Maybe is being used. What is the solution here?

\n
    \n
  1. Use fromMaybe with some dummy default value to extract the inner value. The default value will never be used.
  2. \n
  3. Use something like head . dropWhile to act as a kind of \xe2\x80\x9cunsafe find\xe2\x80\x9d.
  4. \n
  5. Bubble the Maybes all the way up and have the factors returned as a list of Maybes.
  6. \n
  7. Some way to tell Haskell \xe2\x80\x9clook, the math checks out, this is safe, just trust me.\xe2\x80\x9d
  8. \n
\n

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

\n

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.

\n

Li-*_*Xia 7

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.