0

注意：当前问题是 对此问题的后续问题。Daniel Wagner 给出了很好的回答。

我试图弄清楚如何为给定类型的 kind派生自然地图* -> *。natmap是 的自然映射，F如果它等于：

总而言之，Daniel Wagner提出了一种算法，该算法推导fmap给定的仿函数是否是协变的，否则会失败。对于contramap和也可以这样做invmap。他们实施fmap并且contramap：

-- COVARIANT

fmap @(F + F') f (Left x) = Left (fmap @F f x)
fmap @(F + F') f (Right x) = Right (fmap @F' f x)
fmap @(F * F') f (x, y) = (fmap @F f x, fmap @F f y)
fmap @(Id) f x = f x
fmap @(Const X) f x = x
fmap @(F -> F') f x = fmap @F' f . x . contramap @F f

fmap @(F . F') f x = fmap @F (fmap @F' f) x
-- OR
fmap @(F . F') f x = contramap @F (contramap @F' f) x

-- CONTRAVARIANT

contramap @(F + F') f (Left x) = Left (contramap @F f x)
contramap @(F + F') f (Right x) = Right (contramap @F' f x)
contramap @(F * F') f (x, y) = (contramap @F f x, contramap @F' f y)
-- contramap @(Id) fails
contramap @(Const X) f x = x
contramap @(F -> F') f x = contramap @F' f . x . fmap @F f

contramap @(F . F') f x = contramap @F (fmap @F' f) x
-- OR
contramap @(F . F') f x = fmap @F (contramap @F' f) x

丹尼尔瓦格纳的回答让我思考。必须可以用派生 的单个算法替换三种算法（派生和fmap）。例如：我们推导出来，并且在这样做的同时发现它是协变的。因此，我们可以定义for 。反之亦然：.contramapinvmapinvmapinvmapdata F a = F (a, a)Ffmap f = invmap f undefinedFdata F' = F' ((a, a) -> Int)contramap g = invmap undefined g

是如何invmap派生的？

基本上，我们调整 Daniel Wagner 的算法：

{- 1 -} invmap @(F + F') f g (Left x) = Left (invmap @F f g x)
{- 2 -} invmap @(F + F') f g (Right x) = Right (invmap @F' f g x)
{- 3 -} invmap @(F * F') f g (x, y) = (invmap @F f g x, invmap @F' f g y)
{- 4 -} invmap @(F -> F') f g x = invmap @F' f g . x . invmap @F g f

{- 5 -} invmap @(F . F') f g x = invmap @F (invmap @F' f g) (invmap @F' g f) x

{- 6 -} invmap @(Id) f g x = f x
{- 7 -} invmap @(Const X) f x = x

关于上面的一些行的一些评论：

5这个想法是invmap @F (invmap @F' a b) (invmap @F' c d)：

  • a处理F出现在协变位置中的协变位置F'，
  • bF处理出现在协变位置中的逆变位置F'，
  • c处理F出现在逆变位置的协变位置F'，
  • d处理F出现在 中的逆变位置的逆变位置F'。

IE。a和d处理协变位置，而b和c处理逆变位置。因此，a = d = f; b = c = g.

6 Id Leafcase 对于逆变函子确实失败了，因为当contramap g被调用时，undefined被放在f's 的位置。Dually：Idleafcase 是唯一f直接用于协变函子的。

为什么它有效？

我认为这个算法之所以有效，是因为一个简单的原因：invmap实际上不必直接使用它的每个参数。此外，当我们尝试将协变处理器用于逆变函子（即 running contramap @Id g x）时，我们会得到一个错误（因为协变处理器是undefined）。

基本上，我的想法来自于实施fmapand contramap，invmap就像phantom是实施fmapandcontramap。

为什么有趣？

分支会产生一些过热。例如：

contramap @(F . F') f x = contramap @F (fmap @F' f) x
-- OR
contramap @(F . F') f x = fmap @F (contramap @F' f) x

除非F和是幻像，否则其中一个案例在检查和F'的整个结构后会失败。有人可能会声称，从两个中选择一个并不能真正归类为过热，并且可以原谅以保持可读性。但是事情变得非常丑陋。我认为以下每种情况都有7个子情况： , , . 这样的代码似乎效率很低。FF'invmapF -> F'F + F'F * F'

所有这些子案例都是由我们对方差的假设产生的。当我们停止invmap只进行派生时，分支就消失了。

问题

这个算法是否产生合法的自然地图？我认为我们无法fmap f = invmap f undefined在合法的情况下证明这一点。相反，我们依赖于我们运行逆变处理器 的事实，即当我们遇到逆变位置（逆变位置相同）时，上面的算法就是这种情况。

PS有人认为Invariant接口不如Profunctors，应该避免。但是，如果我的算法确实是正确的，我认为这对这样的类来说是一个很好的用途。

4

0 回答 0