Как понять <- в нотации do в Haskell с необычной реализацией ">>=" в монаде?
Я программист C++/Rust и из любопытства сейчас изучаю Haskell. Как и ожидалось, я столкнулся с некоторыми препятствиями, пытаясь понять монады:
Я уже читал об определении монад в Wikibook, включая их связь с математическим определением в теории категорий и тремя законами монад. Я также понимаю, что нотация do — это синтаксический сахар для монад, но определенное поведение в блоках do продолжает меня озадачивать.
В некоторых руководствах я заметил, что bind (>>=) часто объясняется как применение второго аргумента (функции) к значению, содержащемуся в первом аргументе, и возврат результата применения функции. Однако с точки зрения законов монады это не единственная возможная реализация. Я не уверен, должен ли bind всегда следовать этому шаблону или это просто обычная реализация.
Если этот шаблон действительно распространен, то мне придется рассмотреть другие реализации. Больше всего меня смущает то, что мы знаем:
do { v <- y; ... } = y >>= (\v -> ...)
Таким образом, значение <- здесь должно быть напрямую связано с реализацией >>=. Но если это не обычная реализация, упомянутая выше, то <- может больше не нести семантику объявления или привязки. Как следует понимать это в таких случаях?
К сожалению, как новичок, я еще не придумал пример необычной, но законопослушной реализации bind, несмотря на все мои усилия.
Вот краткое изложение моих вопросов:
- Существует ли необычная реализация
bind(>>=), которая по-прежнему удовлетворяет законам Монады? - Я считаю, что это необычная реализация
bind. Как понять значение<-в нотацииdo?
Это верно. Я изменю «назначение в стиле C» на рассматриваемые «объявления».
Ваше определение «общего» не имеет смысла: в элементе типа IO a не содержится «значения». Единственный способ понять это — использовать тип (>>=), m a -> (a -> m b) -> m b, и, конечно же, каждая реализация должна соответствовать этому типу.
Это чисто синтаксический сахар. x <- y; z то же самое, что и y >>= (\x -> z), ни больше, ни меньше. Это преобразование на уровне текста. Что на самом деле означают эти символы, не имеет значения.
@n.m.couldbeanAI Я думаю, что причина существования нотации заключается в том, чтобы использовать монаду, чтобы разделить ее на что-то вроде процедурного программирования, и сказать, что я не могу понять <-, чтобы ее отключить, похоже, отказывается от своей первоначальной цели.
Я не уверен, что полностью понимаю, что вы подразумеваете под «отказаться от своей первоначальной цели». Может быть, вы можете расширить это? Обозначение do — это всего лишь сокращение. Это не что иное, как сокращение. Он существует потому, что раздражает писать (и читать) что-то вроде a >>= \x -> m x p >>= \y -> n (y + q), когда можно написать do { x <- a; y <- m x p; n (y + q) }. Второе — это сокращение от первого.
Я не уверен, что вы считаете «необычной реализацией привязки». Возьмем, к примеру, монаду Maybe. Здесь x >>= f не вызывает f, когда x=Nothing, сокращая вычисления. Точно так же do y <- Nothing ; ... не заботится о части .... Для вас это «необычно»?
С одной стороны, действительно невозможно понять <- «в общем» раз и навсегда именно потому, что это программируется. С другой стороны, некоторые закономерности действительно существуют, поэтому, как только вы поймете это для десяти монад, одиннадцатую станет читать гораздо быстрее. Я думаю, что в наши дни вы могли бы показать мне новую монаду, а я мог бы просто прочитать реализацию >>= и разобраться в ней, и я ожидаю, что по мере того, как вы будете практиковаться в чтении реализаций монады, вы тоже доберетесь до этого. (...кроме Cont, этот парень похож на какой-то психоделик; все, что я понимаю, проходит через несколько часов.)
Остерегайтесь интерпретации m a «содержит значение». Монадическое вычисление m a «содержит» значение типа a точно так же, как команда Unix ls «содержит» список имен файлов.
Ответы 2
Возможно, самой простой из них является монада списка, которая реализована как:
instance Monad [] where
return x = [x]
x >>= f = [y | xi <- x, y <- f xi]здесь x >>= f по сути то же самое, что concatMap f x, который, таким образом, для каждого элемента xi в списке x вызывает f для этого элемента, и к результату добавляется список элементов f xi, которые он производит.
Таким образом, это означает, что если мы напишем:
foo :: [Int]
foo = do
xi <- [1, 4, 2, 5]
[xi, xi + 1]это переводится как:
[1, 4, 2, 5] >>= \xi -> [xi, xi + 1]и это, таким образом, для каждого элемента в списке [1,4,2,5] даст x и x+1, поэтому:
ghci> foo
[1,2,4,5,2,3,5,6]
Здесь xi имеет тип Int, а не [Int].
тогда
<-может больше не нести семантику присваивания или привязки в стиле C.
Ну, на самом деле оно не несет в себе семантики присваивания в стиле C, даже с IO. В Haskell вы не присваиваете значения переменным. Вы объявляете переменную, и эта переменная всегда сохраняет одно и то же значение. Таким образом, вы не можете создавать циклы, которые, например, будут манипулировать значением переменной. Неизменяемость — одна из основных особенностей декларативного языка.
Я заметил, что связывание (>>=) часто объясняется как применение второго аргумента (функции) к значению, содержащемуся в первом аргументе, и возврат результата применения функции. Однако с точки зрения законов монады это не единственная возможная реализация.
Оно должно иметь примерно такое значение, основанное на типах и законах монады. С добавлением forall:
class Monad m where
return :: forall a . a -> m a
(>>=) :: forall a b . m a -> (a -> m b) -> m b
...
Один закон, которому должны следовать монады, заключается в том, что для любых a и kreturn a >>= k эквивалентен k a. Отсюда становится совершенно ясно, что для всех монад a должно в каком-то значимом смысле быть «значением, содержащимся в» return a, а >>= должно каким-то образом извлечь это a и «вернуть результат применения» k в a.
Монады, естественно, могут быть гораздо более сложными. Например, они не обязательно должны содержать ровно один a (см. монаду списка), а также не обязательно, чтобы они «пока» содержали в себе значение — например, IO a — это просто рецепт для создания a, когда бегать. Но благодаря закону, который return a >>= k эквивалентен k a, мы, по крайней мере, гарантируем, что для всех монад существует способ представить «только это значение» return, и когда вы это сделаете, должен быть способ получить его. out и примените к нему некоторую последующую функцию.
(>>=) ничего не перезаписывает — вы не можете переназначить значение, связанное с переменной. Чтобы сделать что-то подобное, вам в конечном итоге понадобится что-то, что сводится к рекурсии, где вы выполняете вызов новой функции с другим значением, связанным с переменной. Но по законам монады (>>=) на самом деле всегда должно представлять собой некоторую последовательность вычислений, которая может перемещать значения только слева направо.
Даже без учета реальных законов уже из типа (>>=) :: forall a b . m a -> (a -> m b) -> m b становится ясно, что если >>= и нужно когда-либо вызывать функцию a -> m b со значением типа a, то это можно сделать только путем получения таких значений из структуры m a. Поскольку функция a -> m b соответствует оставшейся области действия блока do, в области видимости которой находится связанная переменная, вы можете сказать, что если этот раздел блока когда-либо запускался (что не гарантируется и может произойти несколько раз), связанное значение Каким-то образом «пришло» из правой части стрелы-переплета.
Нет, на самом деле, оно само по себе не имеет той же семантики, что и присваивание в стиле C, фактически в Haskell нет присваивания, только объявления.