Действительно ли Haskell чист (есть ли язык, который имеет дело с вводом и выводом вне системы)?

Question

После касания Monads в отношении функционального программирования, делает ли эта функция действительно язык чистым, или это просто еще одна "карта из тюрьмы" для рассуждения компьютерных систем в реальном мире, вне математики на доске?

РЕДАКТИРОВАТЬ:

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

Также я смотрю на вопрос относительно других не очень чистых функциональных языков и некоторых ОО-языков, которые используют хороший дизайн и сравнивают чистоту. Пока что в моем очень ограниченном мире FP, я все еще не поняла чистоту Монад, вам будет приятно узнать, однако мне нравится идея неизменности, которая гораздо важнее в ставках чистоты.

Answer 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 работает аналогично. Хотя выполнение этого требует побочных эффектов, вы можете создавать сложные программы, не выполняя их, в чистом виде. Вы вычисляете описания программ (действия ввода-вывода), а не выполняете их на самом деле.

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

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

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

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

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

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

Этот тип очень похож на Haskell IO, только в Haskell 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) выводит букву А на экран. Если вы оцениваете значение IO, вот так:

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') это действие ввода-вывода, которое сравнивает данный символ с 'v'. Так же, comp('b') это IO-действие, которое сравнивает данный символ с 'b'. В общем, comp это функция, которая принимает символ и возвращает действие ввода-вывода.

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

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

Первый класс

Эти значения 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]

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

Монады

Монады - это некоторые комбинаторы (например, 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, вы можете написать эту функцию самостоятельно.

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

чистота

Главное в чистоте - ссылочная прозрачность и различие между оценкой и исполнением.

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

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

Answer 2

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

Answer 3

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

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

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

vector<char> read(filepath_t)

В нашем новом "чистом стиле" мы обрабатываем это так:

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

Фактически так работает каждое действие Haskell IO.

Итак, теперь у нас есть чистая модель IO. Слава Богу. Если бы мы не могли этого сделать, то, возможно, лямбда-исчисление и машины Тьюринга не являются эквивалентными формализмами, и тогда у нас есть некоторые объяснения. Мы еще не закончили, но две оставленные нам проблемы просты:

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

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

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

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

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

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

Answer 4

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

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

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

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

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

Answer 5

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

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

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

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

Answer 6

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

Answer 7

Действительно ли Haskell чист? [...]

Язык Haskell был чистым; последняя версия - Haskell 1.2. Тогда типmain был:

main :: [Response] -> [Request]

который обычно сокращался до:

main :: Dialogue

где:

type Dialogue = [Response] -> [Request]

а также Response вместе с Request были скромными, хотя и большими типами данных:

Появление ввода-вывода с использованием монадического интерфейса в Haskell все изменило - больше никаких видимых типов данных, только абстрактная спецификация. В результате какIO, return, (>>=) и т.д. теперь специфичны для каждой реализации Haskell.

Итак, теперь вопрос:

• является ли ввод-вывод в вашей реализации Haskell чистым?

Как отмечает Оуэн Стивенс в книге "Подходы к функциональному вводу-выводу":

Ввод / вывод не является особенно активной областью исследований, но новые подходы все еще открываются [...]

Язык Haskell может снова иметь чистую, полностью определенную модель для ввода-вывода...

Answer 8

Нет, это не так. Монада IO нечиста, потому что она имеет побочные эффекты и изменчивое состояние (условия гонки возможны в программах на Haskell, так что... эх... чистый язык FP не знает что-то вроде "условия гонки"). Действительно чистый FP - это Clean с уникальной типизацией, или 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's 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)