Partial work on restructuring which I do not intend to finish.

monoids-in-the-categoy-of-endofunctors.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: e99a010593b8627f3cc837fe8d7be68cf98b9e9b486b8a4caef1070e8b62b2d3
+-- hash: dbc9287122d243040cde8135abd883bf209073c191d5ece40c561f33abfbd4c8
 
 name:           monoids-in-the-categoy-of-endofunctors
 version:        0.1.0.0
@@ -27,7 +27,10 @@ source-repository head
 library
   exposed-modules:
       Category
-      Category.Free
+      Category.Base
+      Category.Constraint
+      Category.Functor.Base
+      Category.Natural
       Category.Star
       Data.Dict
       Data.Recursive
@@ -35,8 +38,8 @@ library
       Paths_monoids_in_the_categoy_of_endofunctors
   hs-source-dirs:
       src
-  default-extensions: BlockArguments ConstraintKinds DataKinds FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude ScopedTypeVariables TypeApplications TypeFamilies TypeOperators Safe
-  ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists
+  default-extensions: BlockArguments ConstraintKinds DataKinds FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
+  ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-safe -Wno-missing-safe-haskell-mode
   build-depends:
       base >=4.13 && <5
     , invariant >=0.5 && <0.6

package.yaml

@@ -24,17 +24,20 @@ default-extensions:
 - LambdaCase
 - MultiParamTypeClasses
 - NoImplicitPrelude
+- PolyKinds
+- RankNTypes
 - ScopedTypeVariables
 - TypeApplications
 - TypeFamilies
 - TypeOperators
-- Safe
 
 ghc-options:
 - -Weverything
 #- -Werror
 - -Wno-missing-export-lists
 - -Wno-missing-import-lists
+- -Wno-safe
+- -Wno-missing-safe-haskell-mode
 
 dependencies:
 - base >= 4.13 && < 5

src/Category.hs

@@ -1,41 +1,27 @@
-{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE UndecidableInstances #-}
-module Category where
+module Category
+    ( module Category.Base
+    , module Category.Functor.Base
+    , module Category.Natural
+    , Monoidal, Unit, Product, monBi, monIdLI, monIdRI, monIdLE, monIdRE, monAssocL, monAssocR
+    , BiEndo, biendomap
+    , ProEndo, diendomap
+    , Bi, bimap
+    , Pro, dimap
+    , Semigroup, append
+    , Monoid, empty
+    , Applicative, pure, ap
+    , Monad, join
+    ) where
 
-import Category.Start qualified as Star
-import Control.Category (Category, id, (.))
-import Data.Dict (Dict (Dict), (:-) (Sub), (\\))
+import Category.Base
+import Category.Constraint
+import Category.Functor.Base
+import Category.Natural
+import Category.Star qualified as Star
 import Data.Kind (Type)
 
--- | An unenriched hom.
-type family (~>) :: i -> i -> Type
-type instance (~>) = (->)
-type instance (~>) = (:-)
-
-type Dom (a :: i) = (~>) :: i -> i -> Type
-
--- | An covariant endofunctor in an unenriched category.
-class Category cat => CovariantEndo cat f where
-    coendomap :: cat a b -> cat (f a) (f b)
-
-instance {-# OVERLAPPABLE #-} Star.Functor f => CovariantEndo (->) f where
-    coendomap = Star.fmap
-
--- | A contravariant endofunctor in an unenriched category.
-class Category cat => ContravariantEndo cat f where
-    contraendomap :: cat b a -> cat (f a) (f b)
-
-instance Star.Contravariant f => ContravariantEndo (->) f where
-    contraendomap = Star.contramap
-
--- | An invariant endofunctor (if that's even considered a functor) in an unenriched category.
-class Category cat => InvariantEndo cat f where
-    invendomap :: cat a b -> cat b a -> cat (f a) (f b)
-
-instance {-# OVERLAPPABLE #-} Star.Invariant f => InvariantEndo (->) f where
-    invendomap = Star.invmap
-
 -- | A bi-endofunctor in an unenriched category covariant in both arguments.
 class Category cat => BiEndo cat f where
     biendomap :: cat a c -> cat b d -> cat (f a b) (f c d)
@@ -50,27 +36,6 @@ class Category cat => ProEndo cat f where
 instance {-# OVERLAPPABLE #-} Star.Profunctor f => ProEndo (->) f where
     diendomap = Star.dimap
 
--- | A covariant functor between unenriched categories.
-class (Category dom, Category cod) => Covariant dom cod f where
-    comap :: dom a b -> cod (f a) (f b)
-
-instance {-# OVERLAPPABLE #-} CovariantEndo cat f => Covariant cat cat f where
-    comap = coendomap
-
--- | A contravariant functor between unenriched categories.
-class (Category dom, Category cod) => Contravariant dom cod f where
-    contramap :: dom b a -> cod (f a) (f b)
-
-instance {-# OVERLAPPABLE #-} ContravariantEndo cat f => Contravariant cat cat f where
-    contramap = contraendomap
-
--- | An invariant functor (if that's even considered a functor) between unenriched categories.
-class (Category dom, Category cod) => Invariant dom cod f where
-    invmap :: dom a b -> dom b a -> cod (f a) (f b)
-
-instance {-# OVERLAPPABLE #-} InvariantEndo cat f => Invariant cat cat f where
-    invmap = invendomap
-
 -- | A bifunctor in an unenriched category covariant in both arguments.
 class (Category dom, Category cod) => Bi dom cod f where
     bimap :: dom a c -> dom b d -> cod (f a b) (f c d)
@@ -125,7 +90,7 @@ instance {-# OVERLAPPABLE #-} Star.Monoid s => Monoid (->) s where
     empty () = Star.mempty
 
 -- | An applicative functor.
-class (Monoidal cat, CovariantEndo cat f) => Applicative cat f where
+class (Monoidal cat, Endofunctor cat f) => Applicative cat f where
     pure :: a `cat` f a
     ap :: Product cat (f (a `cat` b)) (f a) `cat` f b
 
@@ -140,16 +105,6 @@ class Applicative cat m => Monad cat m where
 instance {-# OVERLAPPABLE #-} Star.Monad m => Monad (->) m where
     join = Star.join
 
-newtype Nat f g = Nat { runNat :: forall a. f a ~> g a }
-
-type instance (~>) = Nat
-
-type D (hom :: (i -> j) -> (i -> j) -> Type) = (~>) :: j -> j -> Type
-
-instance (nat ~ Nat, Category (D nat)) => Category (nat :: (i -> j) -> (i -> j) -> Type) where
-    id = Nat id
-    Nat f . Nat g = Nat (f . g)
-
 class AnyC a
 instance AnyC a
 

src/Category/Base.hs

@@ -0,0 +1,15 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+module Category.Base
+    ( module Control.Category
+    , type (~>)
+    , Post
+    ) where
+
+import Control.Category (Category, id, (.))
+import Data.Kind (Type)
+
+-- | An unenriched hom.
+type family (~>) :: i -> i -> Type
+type instance (~>) = (->)
+
+type Post f = forall a. f a

src/Category/Constraint.hs

@@ -0,0 +1,20 @@
+{-# LANGUAGE RankNTypes #-}
+module Category.Constraint
+    ( module Data.Dict
+    , (:-) (Sub)
+    , (\\)
+    ) where
+
+import Category.Base
+import Data.Dict
+
+newtype a :- b = Sub (a => Dict b)
+
+type instance (~>) = (:-)
+
+(\\) :: a => (b => c) -> (a :- b) -> c
+r \\ Sub Dict = r
+
+instance Category (:-) where
+    id = Sub Dict
+    f . g = Sub (Dict \\ f \\ g)

src/Category/Free.hs

@@ -1,14 +0,0 @@
-{-# LANGUAGE PolyKinds #-}
-module Category.Free where
-
-import Category
-import Data.Kind (Type)
-
-data FreeCategory (hom :: i -> i -> Type) :: i -> i -> Type where
-    Id :: FreeCategory hom a a
-    Embed :: !(hom a b) -> FreeCategory hom a b
-    Compose :: !(FreeCategory hom b c) -> !(FreeCategory hom a b) -> FreeCategory hom a c
-
-instance Category (FreeCategory hom) where
-    identity = Id
-    compose = Compose

src/Category/Functor/Base.hs

@@ -0,0 +1,67 @@
+{-# LANGUAGE UndecidableInstances #-}
+module Category.Functor.Base
+    ( Phantom, phmap
+    , Endofunctor, emap, Functor, map
+    , ContraEndofunctor, contraemap, ContraFunctor, contramap
+    , InvariantEndofunctor, invemap, InvariantFunctor, invmap
+    ) where
+
+import Category.Base
+import Category.Star qualified as Star
+import Data.Kind (Type)
+
+-- | A type constructor ending in Type which varies freely in its argument.
+--
+-- All Phantom types should also implement Endofunctor and ContraEndofunctor.
+class Category cat => Phantom cat f where
+    phmap :: f a `cat` f b
+
+-- | An endofunctor in an unenriched category which is covariant in its argument.
+--
+-- All Endofunctors should also implement InvariantEndofunctor.
+class Category cat => Endofunctor cat f where
+    emap :: a `cat` b -> f a `cat` f b
+
+instance {-# OVERLAPPABLE #-} Star.Functor f => Endofunctor (->) f where
+    emap = Star.fmap
+
+-- | A functor between unenriched categories which is covariant in its argument.
+--
+-- All Functors should also implement InvariantFunctor.
+class (Category dom, Category cod) => Functor dom cod f where
+    map :: a `dom` b -> f a `cod` f b
+
+instance {-# OVERLAPPABLE #-} Endofunctor cat f => Functor cat cat f where
+    map = emap
+
+-- \ An endofunctor in an unenriched category which is contravariant in its argument.
+--
+-- All ContraEndofunctors should also implement InvariantEndofunctor.
+class Category cat => ContraEndofunctor cat f where
+    contraemap :: b `cat` a -> f a `cat` f b
+
+instance {-# OVERLAPPABLE #-} Star.Contravariant f => ContraEndofunctor (->) f where
+    contraemap = Star.contramap
+
+-- | A functor between unenriched categories which is contravariant in its argument.
+--
+-- All ContraFunctors should also implement InvariantFunctor.
+class (Category dom, Category cod) => ContraFunctor dom cod f where
+    contramap :: b `dom` a -> f a `cod` f b
+
+instance {-# OVERLAPPABLE #-} ContraEndofunctor cat f => ContraFunctor cat cat f where
+    contramap = contraemap
+
+-- | An endofunctor-like type in an unenriched category which is parametric in its argument.
+class Category cat => InvariantEndofunctor cat f where
+    invemap :: a `cat` b -> b `cat` a -> f a `cat` f b
+
+instance {-# OVERLAPPABLE #-} Star.Invariant f => InvariantEndofunctor (->) f where
+    invemap = Star.invmap
+
+-- | An endofunctor-like type between unenriched categories which is parametric in its argument.
+class (Category dom, Category cod) => InvariantFunctor dom cod f where
+    invmap :: a `dom` b -> b `dom` a -> f a `cod` f b
+
+instance {-# OVERLAPPABLE #-} InvariantEndofunctor cat f => InvariantFunctor cat cat f where
+    invmap = invemap

src/Category/Natural.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- | The category of natural transformations.
+module Category.Natural where
+
+import Category.Base
+import Data.Kind (Type)
+
+newtype Nat f g = Nat { runNat :: forall a. f a ~> g a }
+
+type instance (~>) = Nat
+
+type ChildHom (nat :: (i -> j) -> (i -> j) -> Type) = (~>) :: j -> j -> Type
+
+instance (nat ~ Nat, Category (ChildHom nat)) => Category (nat :: (i -> j) -> (i -> j) -> Type) where
+    id = Nat id
+    Nat f . Nat g = Nat (f . g)

src/Category/Star.hs

@@ -12,7 +12,6 @@ module Category.Star
     ) where
 
 import Control.Applicative        (Applicative, pure, (<*>))
-import Control.Category           (Category, id, (.))
 import Control.Monad              (Monad, join)
 import Data.Bifunctor             (Bifunctor, bimap)
 import Data.Functor               (Functor, fmap)

src/Data/Dict.hs

@@ -1,16 +1,5 @@
 {-# LANGUAGE RankNTypes #-}
 module Data.Dict where
 
-import Control.Category (Category, id, (.))
-
 data Dict c where
     Dict :: c => Dict c
-
-newtype a :- b = Sub (a => Dict b)
-
-(\\) :: a => (b => c) -> (a :- b) -> c
-r \\ Sub Dict = r
-
-instance Category (:-) where
-    id = Sub Dict
-    f . g = Sub (Dict \\ f \\ g)

src/Data/Recursive.hs

@@ -1,27 +1,21 @@
-{-# LANGUAGE PolyKinds #-}
 module Data.Recursive where
 
 import Category
-import Category.Good qualified as Good
 import Data.Kind (Type)
 import Data.Maybe (Maybe (Nothing, Just))
 
 type family Base (t :: i) :: i -> i
 
-class (Category cat, CovariantEndo cat (Base t)) => Recursive cat (t :: i) where
+class (Category cat, Endofunctor cat (Base t)) => Recursive cat (t :: i) where
     project :: cat t (Base t t)
 
-class (Category cat, CovariantEndo cat (Base t)) => Corecursive cat (t :: i) where
+class (Category cat, Endofunctor cat (Base t)) => Corecursive cat (t :: i) where
     embed :: cat (Base t t) t
 
 data N = Z | S N
 
 type instance Base N = Maybe
 
-instance Good.Covariant Maybe where
-    comap _ Nothing  = Nothing
-    comap f (Just x) = Just (f x)
-
 instance Recursive (->) N where
     project Z     = Nothing
     project (S n) = Just n
@@ -36,8 +30,8 @@ data FinF (r :: N -> Type) (n :: N) :: Type where
 
 type instance Base Fin = FinF
 
-instance CovariantEndo Nat FinF where
-    coendomap (Nat f) = Nat \case
+instance Endofunctor Nat FinF where
+    emap (Nat f) = Nat \case
         FZF -> FZF
         (FSF r) -> FSF (f r)
 
@@ -56,8 +50,8 @@ data VecF (a :: Type) (r :: N -> Type) (n :: N) :: Type where
 
 type instance Base (Vec a) = VecF a
 
-instance CovariantEndo Nat (VecF a) where
-    coendomap (Nat f) = Nat \case
+instance Endofunctor Nat (VecF a) where
+    emap (Nat f) = Nat \case
         VZF -> VZF
         (VSF x r) -> VSF x (f r)
 
@@ -69,7 +63,7 @@ instance Recursive Nat (Vec a) where
 type Algebra cat t a = t a `cat` a
 
 cata :: Recursive cat t => Algebra cat (Base t) a -> t `cat` a
-cata alg = alg . coendomap (cata alg) . project
+cata alg = alg . emap (cata alg) . project
 
 newtype Ixr a n = Ixr { getIxr :: Vec a n -> a }