Understanding Identity functor

Question

I am working my way through this tutorial. As documented in the tutorial, I copied some code as below, to represent `functor composition` and `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)) ``` Now, this is what the tutorial states about `identity functor`: ``` Composition with the identity functor in the same category is as expected. F∘IdB = F IdA∘F = F ``` What I am stuck at is trying to think of it in terms of functor composition as represented by `FComp` in the code above. An example below: ``` $ 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 Mayb…

Accepted Answer

Like many equations in Haskell-applied category theory, F ∘ IdB ≡ IdA ∘ F ≡ F should really just be read as equivalences. `FComp Id Maybe Int` is very much not the same thing as `FComp Maybe Id Int` to the type checker; however you can easily write

```
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
```

which implies that both types contain the same information1. That's what we mean by saying they're isomorphic.

1No information is lost in either direction, since `idFunctorIso' . idFunctorIso ≡ id` (as follows from the functor law `fmap id ≡ id`, together with the fact that `unC` and `unId` are simple inverses of the newtype constructors).

Understanding Identity functor

Solution

Problem