Haskell - the impossible is possible?

It is known that the task of determining whether a certain function is true for Integer -> Boolat least one number is computationally insoluble. However, something that at first glance seems to be just such an oracle (namely, a function (Integer -> Bool) -> Maybe Integer) will be described in this article.

To begin with, we will set our type of natural numbers, almost literally following their usual mathematical definition (why this will be needed in the future):

dataNat = Zero | SuccNatderiving (Eq, Ord, Show)

In other words, a positive integer is either zero or some positive integer increased by one ( Succfrom the word successor).

Also, for convenience, we define the basic operations (addition, multiplication, conversion from Integer) on numbers in this representation:

instanceNumNatwhereZero + y = y
    Succ x + y = Succ (x + y)
    Zero * y = ZeroSucc x * y = y + (x * y)
    fromInteger 0 = Zero
    fromInteger n = Succ (fromInteger (n-1))

So far, it seems, nothing special in terms of differences of this type from the usual Integer.

Recall that we want a function of the form (Nat -> Bool) -> Maybe Nat, the result of which will be the number on which the input function returns True, or Nothingif there is no such number. A first approximation may be, for example, a similar function:

lyingSearch :: (Nat -> Bool) -> NatlyingSearch f | f Zero = Zero
              | otherwise = Succ (lyingSearch (f . Succ))

In fact, it is almost obvious that if the desired number exists, this function will return the correct answer. Indeed, if f Zero == True, then the return value will be Zero- right. Otherwise, the function will return x+1where x- the value at which the function f(x+1)is true - is also true.
However, this function has a name lyingSearchin vain : in the case when the required number is not there, the function will go to recursion at every step and will return, in fact, infinity: Succ (Succ (Succ (...where nesting will never end. Because of laziness, Haskellthis is a normal situation. But infinity is not the desired answer - therefore, in this case, the function "lies".

Interestingly, a fully working solution can be made based on the function abovelyingSearch. Consider a function searchdefined as follows:

search f | f possibleMatch = Just possibleMatch
         | otherwise = Nothingwhere
    possibleMatch = lyingSearch f

At first glance, it is not clear how this will work, and whether it will. Let's check with simple examples:

ghci> search (\x -> x*x == 16) -- такое работало и для lyingSearchJust (Succ (Succ (Succ (SuccZero))))
ghci> search (\x -> x*x == 15)
Nothing

That is, the function searchcorrectly determined that there is no natural number with a square equal to fifteen.

In fact, if you look, then everything is simple. Having received a lyingSearchpossible result (which is always a valid type value Nat), we simply pass it to the input of the function fand check the return value. If the desired number exists, then (as already explained earlier) possibleMatch- this is the number, and therefore the check will be successful. Otherwise, because fcompleted for any input value, we will receive Falseand return Nothing.

A function searchreally works for any predicate (function Nat->Bool), and terminates in a finite time (of course, provided thatfalso terminates for any type value Nat). However, the termination condition ffor any argument passed is very strong, and it is it that strongly limits the set of permissible predicates: for example, when there f x = x*x + 1 == xis an infinite loop. It would seem that this is not so, because such a function ends for any number? It turns out that for anyone other than the already mentioned futility: to the left and right of the equal sign will be infinitely nested Succ (Succ (Succ (..., and accordingly it will be impossible to determine whether the left and right sides are equal. It is for this reason that it is impossible to use this function to create a similar type Integer.

Now you can explain in simple words why and how everything works for always-ending functions. After all, iffends at the infinity passed to it, that is, the sequence Succ (Succ (Succ (..., which means that in any case it uses (reveals) no more than some fixed number of constructors Succ.

In essentially the same way, you can create functions like searchfor other types. Relatively simple examples are also real numbers, each represented as an endless list of numbers (see Seemingly Impossible Functional Programs ). On hackage there is a generic package infinite-search , which provides the appropriate monad and related functions.

PS: this article is a little supplemented by a “retelling” of Searchable Data Types , therefore it is not marked as a translation.