用invmap统一推导fmap/contramap的算法是否生成合法自然映射？

注意：当前问题是相关问题的后续，Daniel Wagner此前已给出优质解答。

我正在尝试为种类为* -> *的给定类型推导自然映射（natural map）。对类型构造子F而言，natmap作为自然映射对应以下四类实现：

• 若F为协变（covariant），对应fmap :: (a -> b) -> F a -> F b
• 若F为逆变（contravariant），对应contramap :: (b -> a) -> F a -> F b
• 若F为不变（invariant），对应invmap :: (a -> b) -> (b -> a) -> F a -> F b
• 若F为Phantom类型，对应phantom :: F a -> F b

此前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的解答给了我新的思路：可以将分别推导fmap、contramap、invmap的三个算法统一为仅推导invmap的单一算法。比如对data F a = F (a, a)推导invmap的过程中可判断它是协变的，因此可以为F定义fmap f = invmap f undefined；同理对data F' a = F' ((a, a) -> Int)，可定义contramap g = invmap undefined g。

invmap的推导规则 #

我对Daniel Wagner的算法调整后得到的invmap推导规则如下：

{- 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逆变位置

其中a和d处理协变位置，b和c处理逆变位置，因此替换为a = d = f，b = c = g。

⁶ Id的叶子节点规则对逆变函子会失败，因为调用contramap g时会给f传入undefined；对偶地，对协变函子而言，Id叶子节点是唯一直接使用f的规则。

算法的可行性依据 #

我认为该算法可行的核心原因是invmap不需要强制使用所有入参。当我们尝试为逆变函子调用协变处理器（比如执行contramap @Id g x）时，会因为协变处理器为undefined触发错误，正好对应不符合对应方差的情况。

这个思路本质上是通过invmap实现fmap和contramap，和用fmap和contramap实现phantom的逻辑一致。

算法的价值 #

多分支的推导逻辑会产生额外开销，比如：

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'都是phantom类型，否则总有一个分支在遍历完F和F'的完整结构后推导失败。有人可能认为二选一的分支开销很低，为了可读性可以接受，但推导invmap时分支会变得非常繁琐：F -> F'、F + F'、F * F'每类都有7个子情况，代码效率极低。

这些分支都是由我们对方差的预设判断产生的，取消方差预设、仅推导invmap即可完全消除这些分支。

核心问题 #

我提出的该算法是否能生成符合定律的自然映射？我认为无法直接证明对合法实例而言fmap f = invmap f undefined成立，但算法的规则保证了仅当遇到逆变位置时才会调用逆变处理器（协变同理），是否可以基于该性质确保生成的映射符合定律？

附言：有观点认为Invariant接口不如Profunctor，应当避免使用，但如果我的算法正确，这会是Invariant类的一个很好的应用场景。

内容的提问来源于stack exchange，提问作者Zhiltsoff Igor