Comment by cruegge

A more advanced example of mutual recursion: it's possible to perform an exhaustive search over the "Cantor space" of all infinite sequences of bits that either finds a sequence satisfying a (total, computable) predicate or determines that such a sequence doesn't exist. That is to say, there's a function `search`,

    type Cantor = Natural -> Bit
    search :: (Cantor -> Bool) -> Maybe Cantor

that returns in finite time if its argument does.

Source: https://math.andrej.com/2007/09/28/seemingly-impossible-func...