Является ли Haskell действительно чистым (есть ли какой-либо язык, который занимается вводом и выходом вне системы)?

Ответ 1

Возьмите следующий мини-язык:

data Action = Get (Char -> Action) | Put Char Action | End

Get f означает: прочитайте символ c и выполните действие f c.

Put c a означает: записать символ c и выполнить действие a.

Здесь программа, которая печатает "xy", затем запрашивает две буквы и печатает их в обратном порядке:

Put 'x' (Put 'y' (Get (\a -> Get (\b -> Put b (Put a End)))))

Вы можете манипулировать такими программами. Например:

conditionally p = Get (\a -> if a == 'Y' then p else End)

У этого есть тип Action -> Action - он принимает программу и дает другую программу, которая сначала запрашивает подтверждение. Здесь другое:

printString = foldr Put End

У этого типа String -> Action - он берет строку и возвращает программу, которая записывает строку, например

Put 'h' (Put 'e' (Put 'l' (Put 'l' (Put 'o' End)))).

IO в Haskell работает аналогично. Хотя выполнение требует выполнения побочных эффектов, вы можете создавать сложные программы, не выполняя их, чистым способом. Вы вычисляете описания программ (действия IO), а не выполняете их.

В языке типа C вы можете написать функцию void execute(Action a), которая фактически выполнила программу. В Haskell вы указываете это действие, написав main = a. Компилятор создает программу, которая выполняет действие, но у вас нет другого способа выполнить действие (кроме грязных трюков).

Очевидно, что Get и Put - это не только параметры, вы можете добавить много других вызовов API к типу данных ввода-вывода, например, работать с файлами или concurrency.

Добавление значения результата

Теперь рассмотрим следующий тип данных.

data IO a = Get (Char -> Action) | Put Char Action | End a

Предыдущий тип Action эквивалентен IO (), то есть значение IO, которое всегда возвращает "единица", сравнимое с "void".

Этот тип очень похож на Haskell IO, только в Haskell IO - абстрактный тип данных (у вас нет доступа к определению, только для некоторых методов).

Это IO-действия, которые могут закончиться некоторым результатом. Значение, подобное этому:

Get (\x -> if x == 'A' then Put 'B' (End 3) else End 4)

имеет тип IO Int и соответствует программе C:

int f() {
  char x;
  scanf("%c", &x);
  if (x == 'A') {
    printf("B");
    return 3;
  } else return 4;
}

Оценка и выполнение

Есть разница между оценкой и выполнением. Вы можете оценить любое выражение Haskell и получить значение; например, оценить 2 + 2:: Int в 4:: Int. Вы можете выполнять только выражения Haskell, которые имеют тип IO a. Это может иметь побочные эффекты; выполнение Put 'a' (End 3) помещает букву a в экран. Если вы оцениваете значение ввода-вывода, например:

if 2+2 == 4 then Put 'A' (End 0) else Put 'B' (End 2)

вы получаете:

Put 'A' (End 0)

Но побочных эффектов нет - вы только выполнили оценку, которая безвредна.

Как бы вы перевели

bool comp(char x) {
  char y;
  scanf("%c", &y);
  if (x > y) {       //Character comparison
    printf(">");
    return true;
  } else {
    printf("<");
    return false;
  }
}

в значение IO?

Исправьте некоторый символ, скажем 'v'. Теперь comp('v') - это действие IO, которое сравнивает данный символ с 'v'. Аналогично, comp('b') - это действие IO, которое сравнивает данный символ с 'b'. В общем случае comp - это функция, которая берет символ и возвращает действие IO.

Как программист на C, вы можете утверждать, что comp('b') является логическим. В C оценка и исполнение идентичны (то есть они означают одно и то же или происходят одновременно). Не в Хаскелле. comp('b') оценивается в какое-то действие IO, которое после выполнения дает логическое значение. (Точно, он вычисляется в блок кода, как указано выше, только с заменой "b" на x.)

comp :: Char -> IO Bool
comp x = Get (\y -> if x > y then Put '>' (End True) else Put '<' (End False))

Теперь comp 'b' оценивается в Get (\y -> if 'b' > y then Put '>' (End True) else Put '<' (End False)).

Это также имеет смысл математически. В C, int f() - функция. Для математика это не имеет смысла - функция без аргументов? Пункт функций - принимать аргументы. Функция int f() должна быть эквивалентна int f. Это не так, потому что функции в C смешивают математические функции и действия IO.

Первый класс

Эти значения ввода-вывода являются первоклассными. Так же, как вы можете иметь список списков кортежей целых чисел [[(0,2),(8,3)],[(2,8)]], вы можете создавать сложные значения с помощью IO.

 (Get (\x -> Put (toUpper x) (End 0)), Get (\x -> Put (toLower x) (End 0)))
   :: (IO Int, IO Int)

Кортеж операций ввода-вывода: сначала читает символ и печатает его в верхнем регистре, второй читает символ и возвращает его в нижнем регистре.

 Get (\x -> End (Put x (End 0))) :: IO (IO Int)

Значение IO, которое считывает символ x и заканчивается, возвращая значение IO, которое записывает x на экран.

Haskell имеет специальные функции, которые позволяют легко манипулировать значениями ввода-вывода. Например:

 sequence :: [IO a] -> IO [a]

который принимает список IO-действий и возвращает действие IO, которое выполняет их последовательно.

Монады

Монады - это некоторые комбинаторы (например, conditionally выше), которые позволяют писать программы более структурно. Там функция, которая состоит из типа

 IO a -> (a -> IO b) -> IO b

который задает IO a, а функция a → IO b возвращает значение типа IO b. Если вы пишете первый аргумент как функцию C a f() и второй аргумент как b g(a x), он возвращает программу для g(f(x)). Учитывая вышеописанное определение Action/IO, вы можете написать эту функцию самостоятельно.

Обратите внимание, что монады не являются существенными для чистоты - вы всегда можете писать программы, как я сделал выше.

Purity

Существенная вещь о чистоте - это ссылочная прозрачность и различение оценки и исполнения.

В Haskell, если у вас есть f x+f x, вы можете заменить его на 2*f x. В C, f(x)+f(x) вообще не совпадает с 2*f(x), так как f может печатать что-либо на экране или изменять x.

Благодаря чистоте, компилятор обладает гораздо большей свободой и может оптимизироваться лучше. Он может переупорядочить вычисления, в то время как в C он должен думать, что это изменяет значение программы.

Ответ 2

Важно понимать, что в монадах нет ничего особенного - поэтому они определенно не представляют собой карту "выйти из тюрьмы" в этом отношении. Нет никакой компиляции (или другой) магии, необходимой для реализации или использования монадов, они определены в чисто функциональной среде Haskell. В частности, sdcvvc показал, как определять монады чисто функционально, без каких-либо ресурсов для реализации backdoor.

Ответ 3

Я очень новичок в функциональном программировании, но вот как я это понимаю:

В haskell вы определяете набор функций. Эти функции не выполняются. Они могут быть оценены.

Там одна функция, в частности, получает оценку. Это постоянная функция, которая создает набор "действий". Эти действия включают в себя оценку функций и выполнение IO и других "реальных" вещей. У вас могут быть функции, которые создают и передают эти действия, и они никогда не будут выполняться, если функция не оценивается с помощью unsafePerformIO или они возвращаются основной функцией.

Итак, программа Haskell - это функция, состоящая из других функций, которая возвращает императивную программу. Сама программа Haskell чиста. Очевидно, что самой императивной программы быть не может. Реальные компьютеры по определению нечисты.

В этом вопросе гораздо больше, и многое из этого - вопрос семантики (человеческий, а не язык программирования). Монады также немного более абстрактны, чем то, что я описал здесь. Но я думаю, что это полезный способ думать об этом в целом.

Ответ 4

Для расширенной версии конструкции IO для sdcwc можно посмотреть пакет IOSpec в Hackage: http://hackage.haskell.org/package/IOSpec p >

Ответ 5

Что значит рассуждать о компьютерных системах "вне математики доски"? Что это за рассуждение? Мертвый расчет?

Побочные эффекты и чистые функции являются предметом точки зрения. Если мы рассматриваем номинально побочную функцию как функцию, которая выводит нас из одного состояния мира в другой, он снова чист.

Мы можем сделать каждую побочную функцию чистой, дав ей второй аргумент, мир и требуя, чтобы он передал нам новый мир, когда это будет сделано. Я больше не знаю C++, но скажу, что read имеет такую ​​подпись:

vector<char> read(filepath_t)

В нашем новом "чистом стиле" мы обрабатываем его следующим образом:

pair<vector<char>, world_t> read(world_t, filepath_t)

На самом деле, как работает каждое действие Haskell IO.

Итак, теперь у нас есть чистая модель ввода-вывода. Слава Богу. Если бы мы не могли этого сделать, то, возможно, Lambda Calculus и Turing Machines не были эквивалентными формализмами, и тогда у нас было бы некоторое объяснение. Мы не совсем сделали, но две проблемы, оставленные нам, легки:

• Что входит в структуру world_t? Описание каждого песчинки, клинка трава, разбитое сердце и золотой закат?

• У нас есть неформальное правило, что мы используем мир только один раз - после каждой операции ввода-вывода мы выбросить мир, который мы использовали с ним. Хотя все эти миры, плавающие вокруг, мы обязаны их перепутать.

Первая проблема достаточно проста. До тех пор, пока мы не разрешаем проверку мира, выясняется, что нам не нужно беспокоиться о том, чтобы хранить что-либо в нем. Нам просто нужно убедиться, что новый мир не равен ни одному предыдущему миру (чтобы компилятор не мог оптимизировать некоторые мировые производственные операции, как это иногда бывает в C++). Есть много способов справиться с этим.

Что касается миров, которые смешиваются, мы хотели бы скрыть мир, проходящий внутри библиотеки, чтобы не было возможности добраться до миров и, следовательно, не могли их смешивать. Оказывается, монады - отличный способ скрыть "боковой канал" в вычислении. Введите монаду IO.

Некоторое время назад в списке рассылки Haskell был задан такой же вопрос, как и ваш, и я стал более подробно обращаться к "боковым каналам". Здесь поток Reddit (который ссылается на мою оригинальную электронную почту):

http://www.reddit.com/r/haskell/comments/8bhir/why_the_io_monad_isnt_a_dirty_hack/

Ответ 6

Я думаю об этом так: программы должны что-то делать с внешним миром, чтобы быть полезными. Что происходит (или должно произойти) при написании кода (на любом языке) состоит в том, что вы стараетесь писать максимально чистый, без побочных эффектов код и загорать IO в определенные места.

То, что мы имеем в Haskell, состоит в том, что вы толкнете больше в этом направлении письма, чтобы строго контролировать эффекты. В ядре и во многих библиотеках есть огромное количество чистого кода. Хаскелл действительно все об этом. Монады в Haskell полезны для многих вещей. И одна вещь, для которой они были использованы, - это сдерживание кода, связанного с примесью.

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

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

Ответ 7

Нет, это не так. IO монада нечиста, потому что она имеет побочные эффекты и изменяемое состояние (условия гонки возможны в программах Haskell, так что... чистый язык FP не знает что-то вроде "состояния гонки" ). На самом деле чистый FP является чистым с уникальной типизацией, или Elm с FRP (функциональная реактивная программирование), а не Haskell. Хаскелл - одна большая ложь.

Доказательство:

import Control.Concurrent 
import System.IO as IO
import Data.IORef as IOR

import Control.Monad.STM
import Control.Concurrent.STM.TVar

limit = 150000
threadsCount = 50

-- Don't talk about purity in Haskell when we have race conditions 
-- in unlocked memory ... PURE language don't need LOCKING because
-- there isn't any mutable state or another side effects !!

main = do
    hSetBuffering stdout NoBuffering
    putStr "Lock counter? : "
    a <- getLine
    if a == "y" || a == "yes" || a == "Yes" || a == "Y"
    then withLocking
    else noLocking

noLocking = do
    counter <- newIORef 0
    let doWork = 
        mapM_ (\_ -> IOR.modifyIORef counter (\x -> x + 1)) [1..limit]
    threads <- mapM (\_ -> forkIO doWork) [1..threadsCount]
    -- Sorry, it dirty but time is expensive ...
    threadDelay (15 * 1000 * 1000)
    val <- IOR.readIORef counter
    IO.putStrLn ("It may be " ++ show (threadsCount * limit) ++ 
        " but it is " ++ show val) 

withLocking = do
    counter <- atomically (newTVar 0)
    let doWork = 
        mapM_ (\_ -> atomically $ modifyTVar counter (\x -> 
            x + 1)) [1..limit]
    threads <- mapM (\_ -> forkIO doWork) [1..threadsCount]
    threadDelay (15 * 1000 * 1000)
    val <- atomically $ readTVar counter
    IO.putStrLn ("It may be " ++ show (threadsCount * limit) ++ 
        " but it is " ++ show val)