In Haskell I would do join (***). In Idris flatten (***) does not work ((***) is complicated).
可以将文章内容翻译成中文,广告屏蔽插件可能会导致该功能失效(如失效，请关闭广告屏蔽插件后再试):
问题:
回答1:
In Idris, there's no Functor/Applicative/Monad instances for r -> _ and no Arrow instance for ->, only via Morphism, so using flatten to do \f x -> f x x leads to horribly verbose code full of going from/to Morphism.
You can do it, of course, I'm just not sure it's worth it... compare this:
import Control.Arrow
import Data.Morphisms
both : (a -> b) -> (a, a) -> (b, b)
both = applyMor . applyMor (flatten (Mor (Mor . (***)))) . Mor
to this:
both : (a -> b) -> (a, a) -> (b, b)
both f (x, y) = (f x, f y)
