Как называется эта специальная структура функций?

Предположим, что F - аппликативный функтор с дополнительными законами (с синтаксисом Хаскелла):

• pure (const ()) <*> m === pure ()
• pure (\a b -> (a, b)) <*> m <*> n === pure (\a b -> (b, a)) <*> n <*> m
• pure (\a b -> (a, b)) <*> m <*> m === pure (\a -> (a, a)) <*> m

Какова структура, называемая, если мы опустим (3.)?

Где я могу найти дополнительную информацию об этих законах/структурах?

Комментарии к комментариям

Функторы, удовлетворяющие (2.), часто называются коммутативными.

Возникает вопрос: имеет ли (1.) (2.) и как эти структуры могут быть описаны. Меня особенно интересуют структуры, которые удовлетворяют (1-2.), Но не (3.)

Примеры:

• Монада читателя удовлетворяет (1-3.)
• Монада-писатель на коммутативном моноиде удовлетворяет только (2.)
• Монада F, приведенная ниже, удовлетворяет (1-2.), но не (3.)

Определение F:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
import Control.Monad.State

newtype X i = X Integer deriving (Eq)

newtype F i a = F (State Integer a) deriving (Monad)

new :: F i (X i)
new = F $ modify (+1) >> gets X

evalF :: (forall i . F i a) -> a
evalF (F m) = evalState m 0

Мы экспортируем только типы X, F, new, evalF и экземпляры.

Убедитесь, что выполнено следующее:

• liftM (const ()) m === return ()
• liftM2 (\a b -> (a, b)) m n === liftM2 (\a b -> (b, a)) n m

С другой стороны, liftM2 (,) new new не может быть заменено на liftM (\a -> (a,a)) new:

test = evalF (liftM (uncurry (==)) $ liftM2 (,) new new)
    /= evalF (liftM (uncurry (==)) $ liftM (\a -> (a,a)) new)

Комментарии к C. A. McCann answer

Имеет набросок доказательства того, что из (1.) следует (2.)

pure (,) <*> m <*> n

=

pure (const id) <*> pure () <*> (pure (,) <*> m <*> n)

=

pure (const id) <*> (pure (const ()) <*> n) <*> (pure (,) <*> m <*> n)

=

pure (.) <*> pure (const id) <*> pure (const ()) <*> n <*> (pure (,) <*> m <*> n)

=

pure const <*> n <*> (pure (,) <*> m <*> n)

=... =

pure (\_ a b -> (a, b)) <*> n <*> m <*> n

= см. ниже =

pure (\b a _ -> (a, b)) <*> n <*> m <*> n

=... =

pure (\b a -> (a, b)) <*> n <*> m

=

pure (flip (,)) <*> n <*> m

Наблюдение

Для недостающей части сначала рассмотрим

pure (\_ _ b -> b) <*> n <*> m <*> n

=... =

pure (\_ b -> b) <*> n <*> n

=... =

pure (\b -> b) <*> n

=... =

pure (\b _ -> b) <*> n <*> n

=... =

pure (\b _ _ -> b) <*> n <*> m <*> n

Лемма

Воспользуемся следующей леммой:

pure f1 <*> m  ===   pure g1 <*> m
pure f2 <*> m  ===   pure g2 <*> m

означает

pure (\x -> (f1 x, f2 x)) m  ===  pure (\x -> (g1 x, g2 x)) m

Я мог бы доказать эту лемму только косвенно.

Недостающая часть

С этой леммой и первым наблюдением мы можем доказать

pure (\_ a b -> (a, b)) <*> n <*> m <*> n

=

pure (\b a _ -> (a, b)) <*> n <*> m <*> n

который был недостающей частью.

Вопросы

Это уже доказано где-то (возможно, в обобщенной форме)?

Примечания

(1.) влечет (2.), но в противном случае (1-3) независимы.

Чтобы доказать это, нам понадобится еще два примера:

• Монада G, приведенная ниже, удовлетворяет (3.), но не (1-2.)
• Монада G', приведенная ниже, удовлетворяет (2-3.), но не (1.)

Определение G:

newtype G a = G (State Bool a) deriving (Monad)

putTrue :: G ()
putTrue = G $ put True

getBool :: G Bool
getBool = G get

evalG :: G a -> a
evalG (G m) = evalState m False

Мы экспортируем только те типы G, putTrue, getBool, evalG и Monad.

Определение G' аналогично определению G со следующими отличиями:

Мы определяем и экспортируем execG:

execG :: G' a -> Bool
execG (G m) = execState m False

Мы не экспортируем getBool.