f, g, h :: Клейсли ((-›) e) a b ‹=› f ››› (g &&& h) = (f ››› g) &&& (f ››› h)?

Изменить: мы будем называть стрелку p чистой, если существует такая функция f, которая: p = arr f.

Я пытаюсь лучше понять Arrows в Haskell и хочу выяснить, когда

f >>> (g &&& h) = (f >>> g) &&& (f >>> h), где f, g, h — стрелки.

Очевидно, что в целом это не так. В этом конкретном примере побочные эффекты дублируются справа:

GHCi> c = Kleisli $ \x -> ("AB", x + 1)
GHCi> fst . runKleisli (c >>> c &&& c) $ 1
"ABABAB"
GHCi> fst . runKleisli ((c >>> c) &&& (c >>> c)) $ 1
"ABABABAB"

Очевидно, f >>> (g &&& h) = (f >>> g) &&& (f >>> h), если f чисто.

Я экспериментировал в GHCi с этим оператором для f, g, h :: Kleisli ((->) e) a b, и мне не удалось найти такие значения f, g и h, что f >>> (g &&& h) ≠ (f >>> g) &&& (f >>> h). Действительно ли это утверждение верно для f, g, h :: Kleisli ((->) e) a b, и если да, то может ли это быть действительным доказательством этого: эффект Monad ((->) e) считывается из окружающей среды. Таким образом, результатом применения f является функция, с помощью которой g и h собираются читать из окружения. Независимо от того, где была создана эта функция — она одинакова, поскольку каждый раз применяется к одному и тому же аргументу, поэтому результат чтения из окружения один и тот же, поэтому общий результат тоже одинаков.


haskell monads kleisli arrows reader-monad
person Zhiltsoff Igor    schedule 13.08.2019    source источник
comment
Интересный дополнительный вопрос: какие монады обладают этим свойством? Все ли они изоморфны комбинации Reader и Writer с идемпотентным моноидом?   -  person leftaroundabout    schedule 13.08.2019
comment
@leftaroundabout Я почти уверен, что мы можем добавить Either и Maybe монады в список, поскольку их эффект зависит от последовательности приложений, и, согласно определению (&&&), приложения одинаковы и находятся в том же порядке слева рука и правая рука. Но я могу ошибаться. Что вы думаете?   -  person Zhiltsoff Igor    schedule 13.08.2019

Ответы (1)


arrow_upward
4
arrow_downward

интуитивно

Да, монада (->) e является монадой чтения, и неважно, два чтения мы выполняем или только одно. Запуск f один или два раза не имеет значения, так как он всегда будет давать один и тот же результат с одним и тем же эффектом (чтение).

Ваши рассуждения кажутся мне интуитивно правильными.

Формально

f, g, h :: Kleisli ((->) e) a b по сути означает f, g, h :: a -> (e -> b), удаляя обертку.

Опять же, игнорируя обертку, мы получаем

for all (f :: a -> e -> b) and (g :: b -> e -> c)
f >>> g = (\xa xe -> g (f xa xe) xe)

for all (f :: a -> e -> b) and (g :: a -> e -> c)
f &&& g = (\xa xe -> (f xa xe, g xa xe))

Следовательно:

f >>> (g &&& h)
= { def &&& }
f >>> (\xa xe -> (g xa xe, h xa xe))
= { def  >>> }
(\xa' xe' -> (\xa xe -> (g xa xe, h xa xe)) (f xa' xe') xe')
= { beta }
(\xa' xe' -> (g (f xa' xe') xe', h (f xa' xe') xe'))


(f >>> g) &&& (f >>> h)
= { def >>> }
(\xa xe -> g (f xa xe) xe) &&& (\xa xe -> h (f xa xe) xe)
= { def &&& }
(\xa' xe' -> ((\xa xe -> g (f xa xe) xe) xa' xe', (\xa xe -> h (f xa xe) xe) xa' xe'))
= { beta }
(\xa' xe' -> (g (f xa' xe') xe', h (f xa' xe') xe'))
person chi    schedule 13.08.2019
comment
Обладают ли Either и Maybe монады этим свойством? Я полагаю, что да, так как их эффект зависит от последовательности применений, а согласно определению (&&&) приложения одинаковы и находятся в одном и том же порядке на левой и правой руке. - person Zhiltsoff Igor; 14.08.2019
comment
@ZhiltsoffIgor Думаю, у них это должно быть. - person chi; 14.08.2019