[Haskell-cafe] Re: [Haskell] Seemingly impossible Haskell programs
zunino at di.unipi.it
Sat Sep 29 12:43:51 EDT 2007
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:
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
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.
More information about the Haskell-Cafe