Haskell - the impossible is possible?

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

To begin with, we will define our type of natural numbers, almost literally following their usual mathematical definition (why it will be necessary to see it later):

 data Nat = Zero | Succ Nat deriving (Eq, Ord, Show) 

In other words, a natural number is either a zero or some natural number increased by one ( Succ from the word successor).
')
Also, for convenience, we define the basic operations (addition, multiplication, conversion from Integer ) over numbers in this representation:

 instance Num Nat where Zero + y = y Succ x + y = Succ (x + y) Zero * y = Zero Succ x * y = y + (x * y) fromInteger 0 = Zero fromInteger n = Succ (fromInteger (n-1)) 

So far, it seems, nothing special in terms of the 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 a number on which the input function returns True , or Nothing if there is no such number. The first approximation can be, for example, a similar function:

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

In fact, it is almost obvious that in the case of the existence of the required number this function will return the correct answer. Indeed, if f Zero == True , then the return value will be Zero - true. Otherwise, the function will return x+1 , where x - the value on which the function f(x+1) is true is also true.
However, it’s not for nothing that this function has the name lyingSearch : in the case when there is no desired number, the function will go into recursion at each step and return, in fact, infinity: Succ (Succ (Succ (... , where nesting will never end). Due to Haskell laziness, this is a normal situation, but infinity is not the desired answer — hence, in this case, the function is “lying”.

Interestingly, a fully working solution can be made on the basis of the above lyingSearch function. Consider the search function defined as:

 search f | f possibleMatch = Just possibleMatch | otherwise = Nothing where possibleMatch = lyingSearch f 

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

 ghci> search (\x -> x*x == 16) --     lyingSearch Just (Succ (Succ (Succ (Succ Zero)))) ghci> search (\x -> x*x == 15) Nothing 

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

In fact, if you look, then everything is simple. After receiving a possible result from lyingSearch (which is always a valid value of type Nat ), we simply feed it to the function f and check the return value. If the required number exists, then (as has already been clarified earlier) possibleMatch is just this number, and therefore the check will pass successfully. Otherwise, because f ends for any input value, we get False and return Nothing .

The search function actually works for any predicate (function Nat->Bool ), and ends in a finite time (of course, provided that f also completes for any value of type Nat ). However, the termination condition f for any argument passed is very strong, and it is this that strongly limits the set of admissible predicates: for example, if fx = x*x + 1 == x will be an infinite loop. It would seem that there is not so, because such a function is completed for any number? It turns out that for anyone except for the already mentioned infinity: left and right of the equals sign will be infinitely nested Succ (Succ (Succ (... , and accordingly it will be impossible to determine whether the left and right parts are equal. For this reason it is impossible to use this function for create a similar type for Integer .

It is now possible to explain in simple words why and how everything works for always-ending functions. After all, if f completes at the infinity transmitted to it, that is, the sequence Succ (Succ (Succ (... , it means that in any case it uses (opens) no more than some fixed number of Succ constructors.

In a similar way, you can create functions like search for other types. A relatively simple example is also the real numbers, each represented as an endless list of numbers (see Seemingly Impossible Functional Programs ). On hackage there is a general infinite-search package that provides the corresponding monad and related functions.

PS: this article is a slightly expanded “retelling” of Searchable Data Types , therefore, the translation is not marked.