Skip to content

Commit 061d760

Browse files
author
Marcin Szamotulski
committed
Coyoneda: add some math :)
1 parent 0e8a64d commit 061d760

File tree

1 file changed

+28
-1
lines changed

1 file changed

+28
-1
lines changed

src/Data/Coyoneda.purs

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,19 @@ data CoyonedaF f a i = CoyonedaF (i -> a) (f i)
2626
-- | The `Coyoneda` `Functor`.
2727
-- |
2828
-- | `Coyoneda f` is a `Functor` for any type constructor `f`. In fact,
29-
-- | it is the _free_ `Functor` for `f`.
29+
-- | it is the _free_ `Functor` for `f`, i.e. any natural transformation
30+
-- | `nat :: f ~> g`, can be factor through `liftCoyoneda`. The natural
31+
-- | transformation from `Coyoneda f ~> g` is given by `lowerCoyoneda <<<
32+
-- | hoistCoyoneda nat`:
33+
-- | ```purescript
34+
-- | lowerCoyoneda <<< hoistCoyoneda nat <<< liftCoyoneda $ fi
35+
-- | = lowerCoyoneda (hoistCoyoneda nat (Coyoneda $ mkExists $ CoyonedaF id fi)) (by definition of liftCoyoneda)
36+
-- | = lowerCoyoneda (coyoneda id (nat fi)) (by definition of hoistCoyoneda)
37+
-- | = unCoyoneda map (coyoneda id (nat fi)) (by definition of lowerCoyoneda)
38+
-- | = unCoyoneda map (Coyoneda $ mkExists $ CoyonedaF id (nat fi)) (by definition of coyoneda)
39+
-- | = map id (nat fi) (by definition of unCoyoneda)
40+
-- | = nat fi (since g is a Functor)
41+
-- | ```
3042
newtype Coyoneda f a = Coyoneda (Exists (CoyonedaF f a))
3143

3244
instance eqCoyoneda :: (Functor f, Eq1 f, Eq a) => Eq (Coyoneda f a) where
@@ -78,6 +90,21 @@ unCoyoneda :: forall f g a. (forall b. (b -> a) -> f b -> g a) -> Coyoneda f a -
7890
unCoyoneda f (Coyoneda e) = runExists (\(CoyonedaF k fi) -> f k fi) e
7991

8092
-- | Lift a value described by the type constructor `f` to `Coyoneda f`.
93+
-- |
94+
-- | Note that for any `f` `liftCoyoneda` has a right inverse
95+
-- | `lowerCoyoneda`:
96+
-- | ```purescript
97+
-- | liftCoyoneda <<< lowerCoyoneda $ (Coyoneda e)
98+
-- | = liftCoyoneda <<< unCoyoneda map $ (Coyonead e)
99+
-- | = liftCoyonead (runExists (\(CoyonedaF k fi) -> map k fi) e)
100+
-- | = liftCoyonead (Coyoneda e)
101+
-- | = coyoneda id (Coyoneda e)
102+
-- | = Coyoneda e
103+
-- | ```
104+
-- | Moreover if `f` is a `Functor` then `liftCoyoneda` is an isomorphism of
105+
-- | functors with inverse `lowerCoyoneda`: we already showed that
106+
-- | `lowerCoyoneda <<< hoistCoyoneda id = lowerCoyoneda` is its left inverse
107+
-- | whenever `f` is a functor.
81108
liftCoyoneda :: forall f. f ~> Coyoneda f
82109
liftCoyoneda = coyoneda id
83110

0 commit comments

Comments
 (0)