本文介绍了如何映射一对/元组?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
在 Haskell 中,我会做 join (***)
.在 Idris 中,flatten (***)
不起作用((***)
很复杂).
In Haskell I would do join (***)
. In Idris flatten (***)
does not work ((***)
is complicated).
推荐答案
在 Idris 中,没有 Functor
/Applicative
/Monad
实例用于r ->_ 和 ->
没有 Arrow
实例,只能通过 Morphism
,所以使用flatten
来做\外汇 ->f x x
导致非常冗长的代码,充满了从/到 Morphism
.
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
为此:
both : (a -> b) -> (a, a) -> (b, b)
both f (x, y) = (f x, f y)
这篇关于如何映射一对/元组?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!