[Haskell] проверка на _|_ - Декларативное программирование

Здравствуйте, nikov, Вы писали:

N>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>На машине Тьюринга такое сделать можно.

По-нормальному — никак (кстати, зачем это нужно?).
По-извращенски — есть http://haskell.org/haskellwiki/Unamb:

import Data.Unamb
main = print foldr1 unamb $ map (\x -> x `seq` ()) [error "a", error "b", 42]

Учтите, там внутри запускаются потоки и довольно-таки нестандартным образом обрабатываются исключения; кроме того, unamb имеет предусловие, нарушение которого ломает ссылочную прозрачность.

N>>>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>>>На машине Тьюринга такое сделать можно.
T>>

T>>*MainLayout> foldr seq () [1,error "aaa"]
T>>*** Exception: aaa
T>>*MainLayout> foldr seq () [1,2]
T>>()
T>>

К>в 1-м случае мы же () должны получить?

Mea culpa, недосмотрел.

Пусть мне покажут, как проверить невычислимость на машине Тьюринга, тогда я сделаю и на ФЯ.

Здравствуйте, nikov, Вы писали:

N>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>На машине Тьюринга такое сделать можно.

А что есть _|_ на машине тьюринга?

Какой _|_ на хаскеле, вечный цикл или undefined?

А так, запусти процессы, делающие putMVar после успешного seq и жди этой MVar. Собственно unamb делает примерно это.

Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
На машине Тьюринга такое сделать можно.

N>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>На машине Тьюринга такое сделать можно.

*MainLayout> foldr seq () [1,error "aaa"]
*** Exception: aaa
*MainLayout> foldr seq () [1,2]
()

Здравствуйте, nikov, Вы писали:

N>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>На машине Тьюринга такое сделать можно.

Под _|_ понимается бесконечное вычисление? То есть явный undefined мы выкидываем?

Если так, то можно, например, сделать шедулер-запускальщик вычислений, типа описанного здесь в конце раздела 9.3 и использовать его, запуская

1ый шаг над 1ым элементом ->
1ый шаг над 2ым элементом -> 2ой шаг над 1ым элементом ->
1ый шаг над 3им элементом -> 2ой шаг над 2ым элементом -> 3ий шаг над 1ым элементом ->
...

При этом если какой-то шаг заканчивает какое-то вычисление — функция тут же возвращает ().

Здравствуйте, thesz, Вы писали:

N>>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>>На машине Тьюринга такое сделать можно.

T>

T>*MainLayout> foldr seq () [1,error "aaa"]
T>*** Exception: aaa
T>*MainLayout> foldr seq () [1,2]
T>()
T>

в 1-м случае мы же () должны получить?

Здравствуйте, nikov, Вы писали:

N>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>На машине Тьюринга такое сделать можно.

А для МТ приведи алгоритм?

Здравствуйте, palm mute, Вы писали:

PM>По-извращенски — есть http://haskell.org/haskellwiki/Unamb

Да, именно это искал. Спасибо.

Здравствуйте, thesz, Вы писали:

T>Пусть мне покажут, как проверить невычислимость на машине Тьюринга, тогда я сделаю и на ФЯ.

Проверить невычислимость нельзя, но благодаря наличию универсальной машины можно запустить несколько вычислений параллельно, и ждать остановки хотя бы одного из них.

T>>Пусть мне покажут, как проверить невычислимость на машине Тьюринга, тогда я сделаю и на ФЯ.
N>Проверить невычислимость нельзя, но благодаря наличию универсальной машины можно запустить несколько вычислений параллельно, и ждать остановки хотя бы одного из них.

Bottom это не только "нет остановки". Точнее, это самый неинтересный случай.

T>>Пусть мне покажут, как проверить невычислимость на машине Тьюринга, тогда я сделаю и на ФЯ.

N>Проверить невычислимость нельзя, но благодаря наличию универсальной машины можно запустить несколько вычислений параллельно, и ждать остановки хотя бы одного из них.

import Control.Parallel

notABot [] = ()
notABot (x:xs) = (x `pseq` ()) `par` notABot xs

loop = loop

result = 2

test = notABot [loop,result]

main = do
    print test
    putStrLn "Hi!"

Удовлетворительно ль?

А теперь говори, как ты собрался пользоваться результатами работы этой функции?

Здравствуйте, thesz, Вы писали:

T>Удовлетворительно ль?

Не очень

test = notABot [loop, loop]

Здравствуйте, nikov, Вы писали:

N>Как на Haskell написать функцию :: [a] -> (), которая равна (), если список пуст или хотя бы одно значение из списка не _|_, и _|_ в противном случае?
N>На машине Тьюринга такое сделать можно.

import Control.Concurrent
import Control.Exception
import System.IO.Unsafe

notABot [] = return ()
notABot xs = do
  qsem <- newQSem 0
  ths <- mapM (\t -> forkIO $ (evaluate t >> signalQSem qsem)) xs
  waitQSem qsem
  mapM_ killTheads rhs
  return ()

checkBottom = unsafePerformIO . notABot

В данном случае чистота функции checkBottom лежит на моей ответственности. Т.е. при bottom она выдаёт bottom, а в остальных случаях всегда одно и то же значение. Так что IO там только для деталей реализации.
Собственно, в unamb что-то типа этого и сделано.

Здравствуйте, thesz, Вы писали:

T>А теперь говори, как ты собрался пользоваться результатами работы этой функции?

Тут главным образом теоретический интерес.

Здравствуйте, thesz, Вы писали:

T>Bottom это не только "нет остановки". Точнее, это самый неинтересный случай.

А какие еще? Вроде бы только ошибка, но ее перехват, в отличие от незавершающегося вычисления, не представляется затруднительным.

Здравствуйте, nikov, Вы писали:

N>Здравствуйте, thesz, Вы писали:

T>>Bottom это не только "нет остановки". Точнее, это самый неинтересный случай.

N>А какие еще? Вроде бы только ошибка, но ее перехват, в отличие от незавершающегося вычисления, не представляется затруднительным.

К примеру ядерная боеголовка, упавшая на твой дом тоже _|_

Как более приближенный к жизни вариант — вычисление с unsafePerfomIO в ходе которого получаем BSOD

T>>Bottom это не только "нет остановки". Точнее, это самый неинтересный случай.
N>А какие еще? Вроде бы только ошибка, но ее перехват, в отличие от незавершающегося вычисления, не представляется затруднительным.

И как ты это хочешь сделать?

	От:	palm mute
	Дата:	18.05.09 16:04
	Оценка:	45 (2)

От:	thesz	http://thesz.livejournal.com
Дата:	18.05.09 14:15
Оценка:	+1

От:	vshabanov	http://vshabanov-ru.blogspot.com
Дата:	18.05.09 18:38
Оценка:	+1

От:	nikov	http://www.linkedin.com/in/nikov
Дата:	18.05.09 13:36
Оценка:

От:	thesz	http://thesz.livejournal.com
Дата:	18.05.09 13:47
Оценка:

От:	Курилка	http://kirya.narod.ru/
Дата:	18.05.09 14:07
Оценка: