Как именно `IO` >> = работает под капотом?

Объясняя такую ​​концепцию, как Monads, новичку, я думаю, будет полезно избегать какой-либо сложной терминологии Haskell или чего-либо подобного теории категорий. Я думаю, что хороший способ объяснить это - создать мотивацию для функции a -> m b с помощью простого типа, такого как Maybe:

data Maybe = Just a | Nothing

Все или ничего. Но что, если у нас есть функции f :: a -> Maybe b и g :: b -> Maybe c, и нам нужен хороший способ их комбинировать?

andThen :: Maybe a -> (a -> Maybe b) -> Maybe b
andThen Nothing _ = Nothing
andThen (Just a) f = f a

comp :: Maybe Text
comp = f a `andThen` g
  where f g a = etc...

Затем вы можете сказать, что andThen может быть определен для множества типов (в конечном итоге формируя класс типов монад) ... Следующим убедительным примером для меня будет IO. Но как бы вы сами определили andThen для IO? Это привело меня к собственному вопросу ... моя наивная реализация andThenIO была бы такой:

andThenIO :: IO a -> (a -> IO b) -> IO b
andThenIO io f = f (unsafePerformIO io) 

Но я знаю, что на самом деле это не то, что происходит, когда вы используете >>=, используя IO. Глядя на реализацию bindIO в GHC.Base, я вижу следующее:

bindIO :: IO a -> (a -> IO b) -> IO b
bindIO (IO m) k = IO (\ s -> case m s of (# new_s, a #) -> unIO (k a) new_s)

А для unIO это:

unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
unIO (IO a) = a

Кажется, что это как-то связано с монадой ST, хотя мои знания о ST почти ничего ... Полагаю, мой вопрос в том, в чем именно разница между моей наивной реализацией и реализацией, использующей ST? Моя наивная реализация полезна с учетом этого примера или нет, что на самом деле не происходит под капотом (и может быть вводящим в заблуждение объяснением)

Вы не можете реализовать IO самостоятельно, используя только операции, гарантированные Haskell Report (за исключением, конечно, andThen = (>>=), который на самом деле не решает педагогических целей). Вы должны думать о IO как о встроенной в компилятор магии ... потому что это так. Даже «код», который вы видите, когда нажимаете ссылки на источники в Hackage, который, кажется, реализует ввод-вывод, в конечном итоге сводится к минимуму при обращениях к вещам, которые являются еще более примитивной магией и которые требуют существования среды выполнения GHC (написанной на C).

Daniel Wagner 09.08.2018 17:33

Реализация ввода-вывода в базе не является реальной реализацией IO; Все это происходит с помощью магии компилятора. Вы может реализуете своего рода фальшивый ввод-вывод с смоделированными файлами и входами / выходами и в основном делаете State, используя их.

Cubic 09.08.2018 17:35

Внутренняя реализация GHC основана на идее полностью подделка о том, что IO подобен преобразователю состояний, в котором преобразуемым состоянием является состояние реального мира (имеющего тип State# RealWorld). Реализация ST аналогична, но требует, чтобы выполняемые действия были полиморфными в State# s. Оказывается, для ST фикция работает гораздо хуже, чем для IO (хотя нам понадобятся линейные типы, чтобы сделать его пуленепробиваемым). Если вы ищете хорошие примеры Monad, которые могут выражать IO-подобные вещи, я предлагаю вам взглянуть на «операционные монады».

dfeuer 09.08.2018 17:38

Ваш andThenIO слишком ленив. Рассмотрим andThenIO (putStrLn "Hello") (\_ -> putStrLn "Goodbye"): это просто напечатает "Goodbye" и полностью проигнорирует первый putStrLn. Обычно в этом опасность unsafePerformIO. Вам понадобится seq, чтобы он заработал.

sepp2k 09.08.2018 17:40

@ sepp2k Или, более педантично, нам нужен pseq, поскольку мы заботимся о порядке оценки, который seq не гарантирует (IIRC).

chi 09.08.2018 22:10

Связанный: stackoverflow.com/questions/10447914/….

atravers 08.10.2020 13:56
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
5
6
306
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

(Примечание: это отвечает на часть "как объяснить новичку, как работает IO". Это НЕ пытается объяснить взлом RealWorld#, который использует GHC. В самом деле, последний не является хорошим способом представить IO.)

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

Из-за этого, когда я пытался сделать это в прошлом, я обычно пробовал много подходов, пока один из них не «щелкнул» в ментальном паттерне ученика. Знание их биографии очень помогает.

Императивное закрытие

Например, когда учащийся уже знаком с некоторым императивным языком с закрытием, например JavaScript, я обычно говорю им, что они могут притвориться, что весь смысл программы Haskell состоит в том, чтобы сгенерировать закрытие JavaScript, которое затем запускается с использованием реализации JavaScript. В этом вымышленном объяснении тип IO T обозначает непрозрачный тип, инкапсулирующий закрытие JavaScript, которое при запуске выдаст значение типа T, возможно, после возникновения некоторых побочных эффектов - как это может делать JavaScript.

Итак, значение f :: IO String может быть реализовано как

let f = () => {
    print("side effect");
    return "result";
    };

и g :: IO () может быть реализован как

let g = () => {
    print("g here");
    return {};
    };

Теперь, если у вас есть такое закрытие f, как вызвать его из Haskell? Что ж, напрямую это сделать нельзя, поскольку Haskell хочет держать побочные эффекты под контролем. То есть мы не можем сделать f ++ "hi" или f() ++ "hi".

Вместо этого, чтобы «вызвать закрытие», мы можем привязать его к main.

main :: IO ()
main = g

Действительно, main - это закрытие JavaScript, которое генерируется всей программой Haskell, и оно будет вызываться реализацией Haskell.

Хорошо, теперь возникает вопрос: «как вызвать более одного закрытия?». Для этого можно ввести >> и представить, что он реализован как

function andThenSimple(f, g) {
   return () => {
      f();
      return g();
      };
}

или для >>=:

function andThen(f, g) {
   return () => {
      let x = f();
      return g(x)();  // pass x, and then invoke the resulting closure
      };
}

return проще

function ret(x) {
   return () => x;
}

Эти функции требуют времени, чтобы объяснить, но их не так сложно понять, если кто-то понимает замыкания.

Чистый функционал (он же остается бесплатным)

Другой вариант - сохранить все в чистоте. Или, по крайней мере, максимально чисто. Можно притвориться, что IO a - непрозрачный тип, определяемый как

data IO a
   = Return a
   | Output String (IO a)
   | Input (String -> IO a)
   -- ... other IO operations here

а затем представьте, что значение main :: IO () затем "запускается" каким-то императивным механизмом позже. Программа вроде

foo :: IO Int
foo = do
  l <- getLine
  putStrLn l
  putStrLn l
  return (length l)

на самом деле означает, согласно этой интерпретации,

foo :: IO Int
foo = Input (\l -> Output l (Output l (Return (length l))))

Конечно, здесь return = Return, и определение >>= - хорошее упражнение.

Каррирование примесей

Забудьте IO, монады и все такое. Можно лучше понять две простые концепции

a -> b   -- pure function type
a ~> b   -- impure function type

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

Теперь, в функциональном программировании, у нас есть каррирование, которое представляет собой изоморфизм между

(a, b) -> c

и

a -> (b -> c)

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

(a, b) ~> c
   <===>
a ~> (b ~> c)

Немного подумав, можно даже понять, что первый ~> в a ~> (b ~> c) на самом деле неточен. Вышеупомянутая каррированная функция на самом деле не вызывает побочных эффектов, когда передается только a - это передача b, которая запускает выполнение исходной неторопливой функции, вызывая побочные эффекты.

Имея это в виду, мы можем думать о нечистом каррировании как о

(a, b) ~> c
   <===>
a -> (b ~> c)
--^^-- pure!

Как частный случай получаем изоморфизм

(a, ()) ~> c
   <===>
a -> (() ~> c)

Кроме того, поскольку (a, ()) изоморфен a (здесь требуются более убедительные доказательства), мы можем интерпретировать каррирование как

a ~> c
  <===>
a -> (() ~> c)

Теперь, если мы окрестим () ~> c как IO c, мы получим

a ~> c
  <===>
a -> IO c

Ага! Это говорит нам о том, что нам не нужен общий тип нечистой функции a ~> c. Пока у нас есть его частный случай IO c = () ~> c, мы можем представить (с точностью до изоморфизма) любую функцию a ~> c.

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

Я полностью одобряю IO как тип данных, но я думаю, что использование экзистенциальной количественной оценки (с синтаксисом GADT для ясности) является достаточно важной оптимизацией, которую стоит представить даже новичку. Это позволяет конструктору :>>= или :=<<, поэтому >>= занимает постоянное время. Поскольку интерфейс IO не позволяет проводить осмотр, этого достаточно для обеспечения хорошей производительности с постоянным коэффициентом. data IO :: Type -> Type where {Pure :: a -> IO a; (:=<<) :: (a -> IO b) -> IO a -> IO b; PutStr :: String -> IO (); GetLine :: IO String; ...}

dfeuer 09.08.2018 20:23

@dfeuer Я бы согласился. В зависимости от того, сколько FP уже видел новичок, GADT может быть лучшим выбором.

chi 09.08.2018 22:08

Ах, классика продолжается - это наблюдение упоминается Wadler и здесь на SO; см. stackoverflow.com/questions/6647852/…

atravers 05.08.2020 12:12

Другие вопросы по теме