В блоге у Филип(п)а Вадлера вот какой сегодня пост появился.

Рассмотрим тотальные предикаты над потоками булевых значений:

-- в этом потоке на i-ом месте ложь
pos     :: Int -> [Bool] -> Bool
pos i xs = not (xs !! i)

-- свертка логическим И отрицания первых i элементов потока даст истину
run :: Int -> [Bool] -> Bool
run i xs = and (map not (take i xs))

-- первые i элементов потока являют собой циклическое повторение False,True
alt :: Int -> [Bool] -> Bool
alt i x = take i x == take i (cycle [False,True])

-- первые i элементов потока не совпадают с первыми i элементами этого потока
fal :: Int -> [Bool] -> Bool
fal i x = not (take i x == take i x)

После минимального размышления ясно, что для первых трех предикатов можно предъявить поток, для которого этот предикат выполняется. Для четвертого предиката такого потока, ясное дело, не существует. Ясно ли это компьютеру? Можно ли написать универсальную процедуру

exists :: ([Bool] -> Bool) -> Bool
exists p = ????????????

которая бы возвращала True для тотальных предикатов над потоками, для которых есть удовлетворяющий ему поток, и False в противном случае?


См. также пост Martin Escardo Seemingly impossible functional programs, где похожие соображения изложены подробнее.