Думаю, вы уже исчерпали все интересные возможности. Любая Monad m => m a -> m a функция, которую мы могли бы определить, неизбежно будет выглядеть так:
e :: forall m a. Monad m => m a -> m a
e u = u >>= k
where
k :: a -> m a
k = _
В частности, если k = return, e = id. Чтобы e не был id, k должен использовать u нетривиальным образом (например, k = const u и k = flip fmap u . const равняются вашим двум попыткам). В таком случае, однако, u эффекты будут дублироваться, что приведет к тому, что e не станет морфизмом монады для ряда вариантов выбора монады m. Таким образом, единственный морфизм монады, полностью полиморфный в монаде, - это id.
Сделаем аргумент более явным.
Для ясности я на мгновение переключусь на презентацию _15 _ / _ 16 _ / _ 17_. Мы хотим реализовать:
e :: forall m a. Monad m => m a -> m a
e u = _
Чем заполнить правую часть? Самый очевидный выбор - u. Само по себе это означает e = id, что не выглядит интересным. Однако, поскольку у нас также есть join, return и fmap, есть возможность рассуждать индуктивно с u в качестве базового случая. Скажем, у нас есть 25, построенное с использованием имеющихся у нас средств. Помимо самого v, у нас есть следующие возможности:
join (return v), что v и поэтому не сообщает нам ничего нового;
join (fmap return v), что тоже v; и
join (fmap (\x -> fmap (f x) w) v), для некоторых других w :: m a, построенных по нашим правилам, и для некоторых f :: a -> a -> a. (Добавление m слоев к типу f, как в a -> a -> m a, и дополнительных join для их удаления ни к чему не приведет, поскольку тогда нам нужно будет показать происхождение этих слоев, и все в конечном итоге сведется к другим случаям.)
Единственный интересный случай - №3. На этом этапе я воспользуюсь ярлыком:
join (fmap (\x -> fmap (f x) w) v)
= v >>= \x -> fmap (f x) w
= f <$> v <*> w
Следовательно, любая правая часть, отличная от u, может быть выражена в форме f <$> v <*> w, где v и w являются либо u, либо дальнейшими итерациями этого шаблона, в конечном итоге достигающими u на листьях. Однако аппликативные выражения такого рода имеют каноническую форму, полученную с помощью аппликативных законов, чтобы повторно связать все случаи использования (<*>) слева, которые в данном случае должны выглядеть так ...
c <$> u <*> ... <*> u
... с многоточием, обозначающим ноль или более дальнейших вхождений u, разделенных <*>, а c является a -> ... -> a -> a функцией соответствующей арности. Поскольку a полностью полиморфен, c по параметричности должна быть некоторой const-подобной функцией, которая выбирает один из своих аргументов. В таком случае любое такое выражение можно переписать в терминах (<*) и _55 _...
u *> ... <* u
... с многоточием, обозначающим ноль или более дальнейших вхождений u, разделенных либо *>, либо <*, при этом *> справа от <*.
Возвращаясь к началу, все реализации, не являющиеся id кандидатами, должны выглядеть так:
e u = u *> ... <* u
Мы также хотим, чтобы e был морфизмом монады. Как следствие, это тоже должен быть аппликативный морфизм. Особенно:
-- (*>) = (>>) = \u v -> u >>= \_ -> v
e (u *> v) = e u *> e v
Это:
(u *> v) *> ... <* (u >* v) = (u *> ... <* u) *> (v *> ... <* v)
Теперь у нас есть четкий путь к контрпримеру. Если мы воспользуемся аппликативными законами для преобразования обеих сторон в каноническую форму, мы (по-прежнему) получим чередующиеся u и v с левой стороны и все v после всех u с правой стороны. Это означает, что свойство не будет сохраняться для таких монад, как IO, State или Writer, независимо от того, сколько (*>) и (<*) содержится в e, или какие именно значения выбираются const-подобными функциями с обеих сторон. Быстрая демонстрация:
GHCi> e u = u *> u <* u -- Canonical form: const const <$> u <*> u <*> u
GHCi> e (print 1 *> print 2)
1
2
1
2
1
2
GHCi> e (print 1) *> e (print 2)
1
1
1
2
2
2
person
duplode
schedule
26.04.2020
