这种类型是有效的“2 级双函子”吗？

问题描述

rank2classes 包提供了一个 Functor 版本，其中映射函数似乎是类型构造函数之间的自然转换。

按照这个想法，这里有一个 2 级版本的 Bifunctor：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind

type Rank2Bifunctor :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class Rank2Bifunctor b where
  rank2bimap ::
    (forall x. p x -> p' x) -> (forall x. q x -> q' x) -> b p q -> b p' q'

很明显可以给这个类型 Foo 提供一个 Rank2Bifunctor 实例：

data Foo f g = Foo (f Int) (g Int)

instance Rank2Bifunctor Foo where
    rank2bimap tleft tright (Foo f g) = Foo (tleft f) (tright g)

但是嵌套 Bar 和 f 的 g 类型怎么样：

data Bar f g = Bar (f (g Int))

对于初学者来说，我们似乎需要在 Functor p 的签名中要求 rank2bimap，以便能够转换 g 中的 f。>

Bar 是有效的“二阶二元函子”吗？

解决方法

确实，这不是您的 Bifunctor 的实例，因为缺少约束允许您为 f 选择一个逆变函子，然后 rank2bimap 将大致相当于实现 {{1} fmap：

f

如果您添加 rank2bimap id :: (g ~> g') -> Bar f g -> Bar f g' -- covariance of f,kinda (since Bar f g = f (g Int)) type f ~> f' = (forall x. f x -> f' x) 和 f（此处可选）是函子的要求，那么您确实会得到一个二元函子：

g

特别是，要证明双函子定律，您将需要 rank2bimap :: (Functor f,Functor g) => (f ~> f') -> (g ~> g') -> Bar f g -> Bar f' g' 的自由定理，假设 f ~> f' 和 f 是函子，则 f' 满足所有n :: f ~> f'、phi。