用invmap代替fmap和contramap的推导

如何解决用invmap代替fmap和contramap的推导

注意：当前问题是对this one的跟进。它由 a great answer 收到 Daniel Wagner。

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

• fmap :: (a -> b) -> F a -> F b 在协变 F 的情况下，
• contramap :: (b -> a) -> F a -> F b 在逆变 F 的情况下，
• invmap :: (a -> b) -> (b -> a) -> F a -> F b 在不变 F 的情况下，
• 或 phantom :: F a -> F b（如果是幻影 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

Daniel Wagner's answer 让我思考。必须可以用一个派生 fmap 的算法替换三种算法（派生 contramap、invmap 和 invmap）。例如：我们为 invmap 推导出 data F a = F (a,a) 并且在这样做的同时发现 F 是协变的。因此，我们可以为 fmap f = invmap f undefined 定义 F。 data 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

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

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

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

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

⁶Id 叶情况对于逆变函子确实失败，因为当调用 contramap g 时，undefined 被放入 {{ 1}} 的位置。双重：f 叶案例是唯一一个直接将 Id 用于协变函子的案例。

为什么有效？

我认为这个算法可以工作，原因很简单：f 实际上不必直接使用它的每个参数。此外，当我们尝试将 covariant processor 用于逆变函子（即运行 invmap）时，我们会得到一个错误（因为 covariant processor 是 {{1 }}).

基本上，我的想法来自在 contramap @Id g x 方面实现 undefined 和 fmap，就像 phantom is implemented in terms of fmap and contramap 一样。

为什么有趣？

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

contramap

除非 invmap 和 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' 的整个结构后，其中一种情况会失败。人们可能会声称，从两个中选择一个并没有真正归类为过热，并且可以原谅以保持可读性。但是使用 F 时事情变得很糟糕。我认为以下每种情况都有 7 个子情况：F'、invmap、F -> F'。这样的代码似乎效率很低。

所有这些子案例都是由我们对方差的假设生成的。当我们停止仅推导 F + F' 时，分支消失。

问题

此算法是否产生合法的自然地图？我认为我们无法证明 F * F' 是合法的。相反，我们依赖于这样一个事实：我们运行逆变处理器 iff 我们遇到了一个逆变位置（逆变器也是如此），这就是上面算法中的情况。 >

---

P。 S. Some 表明 invmap 接口不如 Profunctor，应该避免使用。但是，如果我的算法确实是正确的，我认为这对于这样的类来说是一个很好的用途。