Является ли `PoE данных a = пустым | Пара монада?
Этот вопрос возникает из этого ответа на примере функтора, который является Аппликативным, но не Монадой: утверждается, что
data PoE a = Empty | Pair a a deriving (Functor,Eq)
не может иметь экземпляр монады, но я не вижу этого с:
instance Applicative PoE where
pure x = Pair x x
Pair f g <*> Pair x y = Pair (f x) (g y)
_ <*> _ = Empty
instance Monad PoE where
Empty >>= _ = Empty
Pair x y >>= f = case (f x, f y) of
(Pair x' _,Pair _ y') -> Pair x' y'
_ -> Empty
Фактическая причина, по которой я считаю это монадой, состоит в том, что она изоморфна Maybe (Pair a) с Pair a = P a a, Они обе монады, оба проходимы, поэтому их состав тоже должен образовывать монаду. О, я просто узнал не всегда.
Какой контр-пример терпит неудачу, какой монадный закон? (и как это выяснить систематически?)
редактировать: я не ожидал такого интереса в этом вопросе. Теперь я должен принять решение, если я приму лучший пример или лучший ответ на "систематически" часть.
Между тем, я хочу представить, как join работает для более простого Pair a = P a a:
P
________/ \________
/ \
P P
/ \ / \
1 2 3 4
он всегда идет по внешнему пути, уступая P 1 4, более известный как диагональ в матричном представлении. Для ассоциативности монады мне нужны три измерения, лучше работает визуализация дерева. На основании ответа Чи, это неудачный пример объединения, и как я могу его понять.
Pair
_________/\_________
/ \
Pair Pair
/\ /\
/ \ / \
Pair Empty Empty Pair
/\ /\
1 2 3 4
Теперь вы делаете join . fmap join сначала сворачивая нижние уровни, для join . join коллапс от корня.
5 ответов
Видимо, это не монада. Одна из монад "join"законы это
join . join = join . fmap join
Следовательно, согласно закону выше, эти два выхода должны быть равны, но это не так.
main :: IO ()
main = do
let x = Pair (Pair (Pair 1 2) Empty) (Pair Empty (Pair 7 8))
print (join . join $ x)
-- output: Pair 1 8
print (join . fmap join $ x)
-- output: Empty
Проблема в том, что
join x = Pair (Pair 1 2) (Pair 7 8)
fmap join x = Pair Empty Empty
Выполнение дополнительного join на тех не делает их равными.
как это выяснить систематически?
join . join имеет тип m (m (m a)) -> m (m a)Итак, я начал с тройного вложенного Pair-of-Pair-of-Pair, используя цифры 1..8, Это работало нормально. Затем я попытался вставить некоторые Empty внутри, и быстро нашел контрпример выше.
Такой подход был возможен, так как m (m (m Int)) содержит только конечное количество целых чисел внутри, и у нас есть только конструкторы Pair а также Empty пытаться.
Для этих проверок я нахожу join закон легче проверить, чем, скажем, ассоциативность >>=,
QuickCheck сразу находит контрпример к ассоциативности.
{-# LANGUAGE DeriveFunctor #-}
import Test.QuickCheck
data PoE a = Empty | Pair a a deriving (Functor,Eq, Show)
instance Applicative PoE where
pure x = Pair x x
Pair f g <*> Pair x y = Pair (f x) (g y)
_ <*> _ = Empty
instance Monad PoE where
Empty >>= _ = Empty
Pair x y >>= f = case (f x, f y) of
(Pair x' _,Pair _ y') -> Pair x' y'
_ -> Empty
instance Arbitrary a => Arbitrary (PoE a) where
arbitrary = oneof [pure Empty, Pair <$> arbitrary <*> arbitrary]
prop_assoc :: PoE Bool -> (Bool -> PoE Bool) -> (Bool -> PoE Bool) -> Property
prop_assoc m k h =
((m >>= k) >>= h) === (m >>= (\a -> k a >>= h))
main = do
quickCheck $ \m (Fn k) (Fn h) -> prop_assoc m k h
Выход:
*** Failed! Falsifiable (after 35 tests and 3 shrinks):
Pair True False
{False->Pair False False, True->Pair False True, _->Empty}
{False->Pair False True, _->Empty}
Pair False True /= Empty
Поскольку вас интересует, как это делать систематически, вот как я нашел контрпример с помощью quickcheck:
{-# LANGUAGE DeriveFunctor #-}
import Control.Monad ((>=>))
import Test.QuickCheck
-- <your code>
Определение произвольного экземпляра для генерации случайного PoEs.
instance (Arbitrary a) => Arbitrary (PoE a) where
arbitrary = do
emptyq <- arbitrary
if emptyq
then return Empty
else Pair <$> arbitrary <*> arbitrary
И тесты по законам монады:
prop_right_id m = (m >>= return) == m
where
_types = (m :: PoE Int)
prop_left_id fun x = (return x >>= f) == f x
where
_types = fun :: Fun Int (PoE Int)
f = applyFun fun
prop_assoc fun gun hun x = (f >=> (g >=> h)) x == ((f >=> g) >=> h) x
where
_types = (fun :: Fun Int (PoE Int),
gun :: Fun Int (PoE Int),
hun :: Fun Int (PoE Int),
x :: Int)
f = applyFun fun
g = applyFun gun
h = applyFun hun
Я не получаю никаких ошибок для законов о личности, но prop_assoc генерирует контрпример:
ghci> quickCheck prop_assoc
*** Failed! Falsifiable (after 7 tests and 36 shrinks):
{6->Pair 1 (-1), _->Empty}
{-1->Pair (-3) (-4), 1->Pair (-1) (-2), _->Empty}
{-3->Empty, _->Pair (-2) (-4)}
6
Не то чтобы это очень помогло понять причину сбоя, оно дает вам место для начала. Если мы посмотрим внимательно, мы увидим, что мы проходим (-3) а также (-2) к третьей функции; (-3) карты для Empty а также (-2) карты к Pairпоэтому мы не можем подчиняться законам одной из двух монад PoE состоит из.
Этот вид потенциала Monad Экземпляр можно кратко описать как "взятие диагонали". Легче понять, почему, если мы используем join презентация. Вот join для Pair типа вы упоминаете:
join (P (P a00 a11) (P a10 a11)) = P a00 a11
Однако взятие диагонали гарантирует только законный join для фиксированной длины (или бесконечных) списков. Это из-за закона ассоциативности:
join . join = join . fmap join
Если n-й список в списке списков не имеет n-го элемента, это приведет к урезанию диагонали: он закончится раньше, чем у его n-го элемента. join . join сначала принимает внешнюю диагональ (списка списков), а join . fmap join сначала берет внутренние диагонали. Это может быть возможно для недостаточно длинного внутреннего списка, который не во внешней диагонали, чтобы обрезать join . fmap join, но это не может повлиять join . join, (Это было бы легче показать с изображением вместо слов.)
Ваш PoE является списочно-подобным типом, который не имеет фиксированной длины (длина равна нулю или двум). Оказывается, что взятие его диагонали не дает нам монады, поскольку потенциальная проблема, обсужденная выше, фактически мешает (как показано в ответе Чи).
Дополнительные примечания:
Это как раз причина
ZipListне монада: быстрое поведение сводится к взятию диагонали.Бесконечные списки изоморфны функциям из натуральных чисел, а списки фиксированной длины изоморфны функциям из натуральных чисел вплоть до подходящего значения. Это означает, что вы можете получить
Monadэкземпляр для них вне экземпляра для функций - и экземпляр, который вы получаете, опять же, сводится к взятию диагонали.
(Размещать это как отдельный ответ, так как он мало похож на другой.)
Фактическая причина, по которой я считаю это монадой, состоит в том, что она изоморфна
Maybe (Pair a)сPair a = P a a, Они обе монады, оба проходимы, поэтому их состав тоже должен образовывать монаду. О, я просто узнал не всегда.
Условия для составления монад m-над-n с n проходимыми являются:
-- Using TypeApplications notation to make the layers easier to track.
sequenceA @n @m . pure @n = fmap @m (pure @n)
sequenceA @n @m . fmap @n (join @m)
= join @m . fmap @m (sequenceA @n @m) . sequenceA @n @m
sequenceA @n @m . join @n
= fmap @m (join @n) . sequenceA @n @m . fmap @n (sequenceA @n @m)
(Существует также sequenceA @n @m . fmap @n (pure @m) = pure @m, но это всегда так.)
В нашем случае мы имеем m ~ Maybe а также n ~ Pair, Соответствующие определения метода для Pair было бы:
fmap f (P x y) = P (f x) (f y)
pure x = P x x
P f g <*> P x y = P (f x) (g y)
join (P (P a00 a01) (P a10 a11)) = P a00 a11 -- Let's pretend join is a method.
sequenceA (P x y) = P <$> x <*> y
Давайте проверим третье свойство:
sequenceA @n @m . join @n
= fmap @m (join @n) . sequenceA @n @m . fmap @n (sequenceA @n @m)
-- LHS
sequenceA . join $ P (P a00 a01) (P a10 a11)
sequenceA $ P a00 a11
P <$> a00 <*> a11 -- Maybe (Pair a)
-- RHS
fmap join . sequenceA . fmap sequenceA $ P (P a00 a01) (P a10 a11)
fmap join . sequenceA $ P (P <$> a00 <*> a01) (P <$> a10 <*> a11)
fmap join $ P <$> (P <$> a00 <*> a01) <*> (P <$> a10 <*> a11)
fmap join $ (\x y z w -> P (P x y) (P z w)) <$> a00 <*> a01 <*> a10 <*> a11
(\x _ _ w -> P x w) <$> a00 <*> a01 <*> a10 <*> a11 -- Maybe (Pair a)
Это явно не то же самое: в то время как любой a значения будут взяты исключительно из a00 а также a11, эффекты a01 а также a10 игнорируются с левой стороны, но не с правой стороны (другими словами, если a01 или же a10 являются NothingRHS будет Nothing, но LHS не обязательно будет так). LHS точно соответствует исчезновению Empty в ответе Чи, а RHS соответствует внутренней диагональной обрезке, описанной в моем другом ответе.
PS: я забыл показать, что потенциальный экземпляр, о котором мы здесь говорим, тот же, который обсуждается в вопросе:
join' :: m (n (m (n a))) -> m (n a)
join' = fmap @m (join @n) . join @m . fmap @m (sequenceA @n @m)
С m ~ Maybe а также n ~ Pair, у нас есть:
join' :: Maybe (Pair (Maybe (Pair a))) -> Maybe (Pair a)
join' = fmap @Maybe (join @Pair) . join @Maybe . fmap @Maybe (sequenceA @Pair @Maybe)
join @Maybe . fmap @Maybe (sequenceA @Pair @Maybe) означает join' приведет к Nothing если нет Nothingгде угодно:
join' = \case
Just (P (Just (P a00 a01)) (Just (P a10 a11))) -> _
_ -> Nothing
Разработка неNothing дело простое:
fmap join . join . fmap sequenceA $ Just (P (Just (P a00 a01)) (Just (P a10 a11)))
fmap join . join $ Just (Just (P (P a00 a01) (P a10 a11)))
fmap join $ Just (P (P a00 a01) (P a10 a11))
Just (P a00 a11)
Следовательно...
join' = \case
Just (P (Just (P a00 _)) (Just (P _ a11))) -> Just (P a00 a11)
_ -> Nothing
... который по сути такой же как:
join = \case
Pair (Pair a00 _) (Pair _ a11) -> Pair (a00 a11)
_ -> Empty