from-cofree.md

Note: Calculation on types

Goal

Let DD be the following type.

type DD = forall w. Comonad w => w A -> w B

DD is isomorphic to simple A -> A -> B function.

Step1: Convert to "for all Functor g"

This step shows DD is isomorphic to DD' below.

type DD = forall w. Comonad w => w A -> w B
type DD' = forall g. Functor g => Cofree g A -> g B

Using Yoneda lemma, w B is isomorphic to the following form

w B ≅ forall g. (Functor g) => (w ~> g) -> g B
    ---- (1)

where ~> denotes the type of natural transformations (which are not necessarily a comonad morphism). Substituting (1) to DD:

DD
 ≅ forall w. Comonad w => w A -> forall g. Functor g => (w ~> g) -> g B
 ≅ forall w g. (Comonad w, Functor g) => w A -> (w ~> g) -> g B 

   ---- (2)

By the universal property of the Cofree comonad, any natural transformation f :: w ~> g has one-to-one correspondence with Comonad morphism f' :: w ~~> Cofree g. Here, the longer wiggled arrow ~~> is used to denote the type of Comonad morphisms rather than mere natural transformation.

Using this isomorphism, DD can be transformed further:

DD
 ≅ forall w g. (Comonad w, Functor g) => w A -> (w ~~> Cofree g) -> g B
 ≅ forall g. Functor g =>
     forall w. (Comonad w) => (w ~~> Cofree g) -> (w A -> g B)
 ≅ forall g. Functor g =>
     forall w. (Comonad w) => (w ~~> Cofree g) -> (w A -> g B)
   ---- (3)

Regard both (w ~~> Cofree g) and (w A -> g B) as two contravariant functors from the category of Comonads to Type, and forall w. (Comonad w) => (w ~~> Cofree g) -> (w A -> g B) as the type of natural transformations between them.

Then, the (contravariant) Yoneda theorem says

(forall w. (Comonad w) => (w ~~> Cofree g) -> (w A -> g B))
  ≅ Cofree g A -> g B

therefore DD is isomorphic to the goal DD'.

DD
 ≅ forall g. Functor g =>
     forall w. (Comonad w) => (w ~~> Cofree g) -> (w A -> g B)
 ≅ forall g. Functor g => Cofree g A -> g B
 = DD'

Step2: Remove forall Functor g

(this step is more handwavy than Step1)

DD'
 ≅ forall g. Functor g => Cofree g A -> g B
 ≅ forall g. Functor g => (A, g (Cofree g A)) -> g B
 ≅ forall g. Functor g => (A, g (A, g (A, Cofree g A))) -> g B
 ≅ A -> forall g. Functor g => g (A, g (A, Cofree g A)) -> g B

• To make a g B value from ga : g (A, g (...)) value, one can only do fmap (f :: (A, g (...)) -> B) ga since g is only a Functor and no value other than ga in the environment provide g _ value from nothing

• f :: (A, g (...)) -> B can not "use" the second argument g (...), because g is an opaque Functor type and also no way to "extract" (...) value out of g. therefore, f must be f = (f' :: A -> B) . fst

• Conversely, given forall g. Functor g => g (A, g (A, Cofree g A)) -> g B, let g = (->) A and pass rec = \a -> (a :> rec) :: Cofree ((->) A) in, then get g B ~ A -> B. this is the right inverse of f ↦ fmap (f . fst) :: g (A, g (A, Cofree g A)) -> g B

Thus

DD'
 ≅ A -> (A -> B)