Что можно доказать о параметрах в лямбда-выражениях, переданных в монады?

Question

Относительно оператора рыбы Монады удовлетворяют ассоциативности.

(h >=> g) >=> f = h >=> (g >=> f) 

Это переводится связать (с лямбда-выражений) выглядит,

\a -> h a >>=(\b -> g b >>= \c -> f c) = 
\a ->(h a >>= \b -> g b)>>= \c -> f c 

, что означает следующее уравнение однозначен

(a -> h a >>= \b -> g b >>= \c -> f c) = h >=> g >=> f 

Это хороший способ понять Монадические композицию.

Однако не все Monadic-коды сохраняют связанные переменные в lambdas. Например,

[1,2] >>= \n -> ['a','b'] >>= \ch -> return (n,ch) = 
[(1,'a'),(1,'b'),(2,'a'),(2,'b')] 

«n» в обратном направлении было получено из верхней лямбда.

В более общем плане,

a -> g a >>= \b -> f a b 

е зависит от А и Б в указанных выше. Определение выше в терминах е, ж, и (> =>) дает

\a -> (\x -> g a) >=> f a 

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

Один из подходов это, пытаясь получить значение из выражения списка синтаксиса

[ (n,ch) | n <- [1, 2], ch <- ['a', 'b'] ] 

Я думаю, что это подразумевает вид симметрии.

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

Answer 1

Нет, никаких ограничений. Как только вы связали лямбду, вы можете сделать anything. Это одна из причин того, что Applicative предпочтительнее Monad, потому что он слабее (и, следовательно, дает вам более сильные ограничения свободы).

([1,2] >>= \n -> "ab" >>= \ch -> return (n,ch)) 
    ≡ (,) <$> [1,2] <*> "ab" 
    ≡ liftA2 (,) [1,2] "ab" 
    ≈ liftA2 (flip (,)) "ab" [1,2] 

Последнее на самом деле не является правильным уравнением; аппликативные законы только гарантии, что значение будет одинаковым для этих выражений^{См комментариев}, но структуры может и будет отличаться.

Prelude Control.Applicative> liftA2 (,) [1,2] "ab" 
[(1,'a'),(1,'b'),(2,'a'),(2,'b')] 
Prelude Control.Applicative> liftA2 (flip (,)) "ab" [1,2] 
[(1,'a'),(2,'a'),(1,'b'),(2,'b')] 

Answer 2

Обращаясь правку, в которой вы считаете, как написать ...

\a -> g a >>= \b -> f a b 

... используя (>=>), ничего на самом деле потеряли в этом случае.Это полезно сделать шаг назад и рассмотреть, как именно (>=>) может быть преобразована в (>>=) и наоборот:

f >=> g = \x -> f x >>= g 
m >>= f = (const m >=> f)() -- const x = \_ -> x 

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

Это, так, что ваш пример можно переписать с помощью второго уравнения:

\a -> g a >>= \b -> f a b 
\a -> (const (g a) >=> \b -> f a b)() 
\a -> (const (g a) >=> f a)() 

Который, за исключением добавленного трюка подачи фиктивный (), что вы получили в вашем вопросе.

Answer 3

Дополнительная идея на ваш вопрос: Монады наиболее общие в том смысле, что эффекты могут зависеть от входов. Монадическое вычисление m, которое принимает входные данные a и производит выходные данные b может быть написано как a -> m b. Поскольку это функция, мы можем определить такие вычисления, используя lambdas, которые могут естественным образом охватывать право. Но эта общность усложняет анализ вычислений как вашего \a -> g a >>= \b -> f a b.

Для arrows (которые занимают пространство между аппликативными функторами и монадами) ситуация несколько отличается. Для общей стрелки вход должен быть явным - вычисление стрелки arr имеет общий тип arr a b. И поэтому вход, который охватывает «вперед» в вычислении стрелки, должен быть явно пронумерован там, используя примитивы Arrow.

Чтобы расширить свой пример

{-# LANGUAGE Arrows #-} 

import Control.Arrow 

bind2 :: (Monad m) => (a -> m b) -> (a -> b -> m c) -> a -> m c 
bind2 g f = \a -> g a >>= \b -> f a b 

стрелкам: Функция f теперь должны взять пару в качестве входных данных (потому что стрелки определяются как принимать одно входное значение). Используя стрелку do обозначения мы можем выразить это как

bind2A :: (Arrow arr) => arr a b -> arr (a, b) c -> arr a c 
bind2A g f = proc a -> do 
       b <- g -< a 
       c <- f -< (a, b) 
       returnA -< c 

Или еще проще с помощью Arrow примитивов:

bind2A' :: (Arrow arr) => arr a b -> arr (a, b) c -> arr a c 
bind2A' g f = (returnA &&& g) >>> f 

Графический:

--------------->[ ] 
    \   [ f ]----> 
    \-->[ g ]-->[ ] 

Будучи менее общими, стрелки позволяют сделать вывод о более информацию о цепи до ее фактического выполнения. Хорошее чтение - Understanding arrows, в котором описывается первоначальная мотивация, стоящая за ними, - для создания парсеров, которые могут избежать утечек пространства, имея статические и динамические части.