haskell - 理解恒等仿函数

Question

我正在努力解决这个 tutorial .如教程中所述，我复制了一些代码如下，以表示 functor composition 和 identity functor:

{-# LANGUAGE FlexibleContexts #-}
module Test where

newtype FComp f g a = C { unC :: f (g a) }

instance (Show (f (g a))) => Show (FComp f g a) where
  show (C x) = "FComp " ++ show x

instance (Functor f, Functor g) => Functor (FComp f g) where
  fmap h (C x) = C (fmap (fmap h) x)

newtype Id a = Identity { unId :: a } deriving Show

instance Functor Id where
    fmap f x = Identity (f (unId x))

现在，这就是教程中关于identity functor 的内容:

Composition with the identity functor in the same category is as expected.
F∘IdB = F  
IdA∘F = F

我所坚持的是试图根据上面代码中 FComp 表示的仿函数组合来考虑它。下面是一个例子:

$ let a = C (Identity (Just (5::Int)))
$ :t a
a :: FComp Id Maybe Int
$ let b = C (Just (Identity (5::Int)))
$ :t b
b :: FComp Maybe Id Int

我想不出一种方法来断言上面示例中表示的 a 和 b 的类型是相同的。我将感谢有关如何根据仿函数组合 考虑identity functor 的指示。

Answer 1

像 Haskell 应用范畴论中的许多方程一样，F ∘ Id_B ≡ Id_A ∘ F ≡ F 实际上应该被理解为等价。 FComp Id Maybe Int 与类型检查器的 FComp Maybe Id Int 非常不同；但是你可以很容易地写

idFunctorIso :: Functor f => FComp f Id a -> f a
idFunctorIso (C fIdca) = fmap unId fIdca

idFunctorIso' :: Functor f => f a -> FComp f Id a
idFunctorIso' fa = C $ fmap Identity fIdc

这意味着两种类型都包含相同的信息¹。这就是我们所说的它们是同构的。

---

¹自 idFunctorIso' 以来，任何方向都不会丢失信息。 idFunctorIso ≡ id(从仿函数法则fmap id ≡ id，连同unC 和unId 很简单新类型构造函数的逆函数)。