[Haskell-cafe] Re: [Haskell] Seemingly impossible Haskell programs
Aaron Denney
wnoise at ofb.net
Sat Sep 29 14:38:40 EDT 2007
On 2007-09-29, Roberto Zunino <zunino at di.unipi.it> wrote:
> 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.
Well, any /computable/ total predicate. This distinction isn't
that relevant when we're talking about predicates we might want to
implement and run, but there is a mathematical distinction.
--
Aaron Denney
-><-
More information about the Haskell-Cafe
mailing list