haskell - 这种类型是有效的 "rank-2 bifunctor"吗？

Question

rank2classes包提供了 Functor 的版本映射函数似乎是类型构造函数之间的自然转换。
按照这个想法，这里是 Bifunctor 的 2 级版本:

{-# 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一个有效的“2 级二元仿函数”？

Answer 1

事实上，这不是你的 Bifunctor 的一个实例。 ，因为缺少约束允许您为 f 选择一个逆变仿函数然后 rank2bimap大致相当于实现 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 , fmap phi . n = n . fmap phi .