[Haskell-cafe] Re: [Haskell] Seemingly impossible Haskell programs

[Roberto Zunino]

Graham Hutton wrote:
> Readers of this list may enjoy the following note by
> Martin Escardo, which shows how to write a number of
> "seemingly impossible Haskell programs" that perform
> exhaustive searches over spaces of infinite size, by
> exploiting some ideas from topology:
> 
>    http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/#more-69

Very nice! The note shows that you can actually compute (forall p) where
p is a *total* predicate over streams of Bool (a.k.a. infinite lazy
lists). Indeed, (writing [] for streams)

  forall :: ([Bool] -> Bool) -> Bool

seems impossible to compute.

Here's what I understood: (which might be wrong, of course!)

This apparent magic relies on the fact that any total predicate over
(total) bool streams, i.e.

  p :: [Bool] -> Bool

can only inspect a _finite_ prefix of the input list.
More importantly, the length of the inspected prefix has an upper bound
which depends _only_ on p and not on the actual input of p. In rough
formulas

 forall p, exists n:nat, forall l:[Bool], forall l':[Bool],
   p l == p (take n l ++ l')

So, with some nice laziness tricks, you can actually check p over "all"
the infinite [Bool] space, using only finite time.

Zun.