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:
factorize n | isPrime n = [n]\n | otherwise = m : factorize (n `div` m)\n where m = find ((==0) . (n `mod`)) [2..]\nRun Code Online (Sandbox Code Playgroud)\nfind 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?
fromMaybe with some dummy default value to extract the inner value. The default value will never be used.head . dropWhile to act as a kind of \xe2\x80\x9cunsafe find\xe2\x80\x9d.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?
\nEdit: 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.
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.