Я думаю, что вы уже исчерпали все интересные возможности. Любая функция 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. Таким образом, единственный монад морфизма, полностью полиморфный c в монаде, является id.
Давайте сделаем аргумент более явным.
Для ясности я на мгновение переключится на презентацию join / return / fmap. Мы хотим реализовать:
e :: forall m a. Monad m => m a -> m a
e u = _
Чем мы можем заполнить правую часть? Самый очевидный выбор - u. Само по себе это означает e = id, что не выглядит интересным. Однако, поскольку у нас также есть join, return и fmap, существует возможность индуктивного рассуждения с u в качестве базового случая. Скажем, у нас есть v :: m a, построенный с использованием имеющихся у нас средств. Помимо самого 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 s для их удаления ни к чему не приведут, так как тогда нам придется показать происхождение этих слоев и тому подобное. в конечном итоге сводится к другим случаям.)
Единственный интересный случай # 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 s на листьях. Аппликативные выражения такого рода, однако, имеют каноническую форму, полученную с помощью аппликативного l aws для повторного сопоставления всех случаев использования (<*>) влево, что в данном случае должно выглядеть следующим образом ...
c <$> u <*> ... <*> u
... с многоточием, равным нулю или более дальнейших вхождений u, разделенных <*>, а c является функцией a -> ... -> a -> a соответствующей арности. Поскольку a является полностью полиморфным c, c, по параметризации, должен быть некоторой const -подобной функцией, которая выбирает один из своих аргументов. При этом любое такое выражение может быть переписано в терминах (<*) и (*>) ...
u *> ... <* u
... с многоточием, равным нулю или более дальнейших вхождений u, разделенных *> или <*, справа от <* нет *>.
Возвращаясь к началу, все реализации-не-1095 * кандидата должны выглядеть следующим образом:
e u = u *> ... <* u
Мы также хотим, чтобы e был морфизмом монады. Как следствие, это также должен быть аппликативный морфизм. В частности:
-- (*>) = (>>) = \u v -> u >>= \_ -> v
e (u *> v) = e u *> e v
То есть:
(u *> v) *> ... <* (u >* v) = (u *> ... <* u) *> (v *> ... <* v)
Теперь у нас есть четкий путь к контрпримеру. Если мы используем аппликативный l aws для преобразования обеих сторон в каноническую форму, мы (все еще) в итоге получим с чередованием u s и v s с левой стороны и со всеми v s после все 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