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/#...
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.