Moved Category to Effect: issue #1636 (#1735)

Author: jamesmckinna

CHANGELOG.md

@@ -58,6 +58,17 @@ Non-backwards compatible changes
   `Codata` which used sized types have been moved inside a new folder named
   `Sized`, e.g. `Codata.Stream` has become `Codata.Sized.Stream`.
 
+#### Moved `Category` modules to `Effect`
+
+* As observed by Wen Kokke in Issue #1636, it no longer really makes sense
+  to group the modules which correspond to the variety of concepts of 
+  (effectful) type constructor arising in functional programming (esp. in haskell) 
+  such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, as this
+  obstructs the importing of the `agda-categories` development into the Standard Library,
+  and moreover needlessly restricts the applicability of categorical concepts to this
+  (highly specific) mode of use. Correspondingly, modules grouped under `*.Categorical.*`
+  which exploited these structures for effectful programming have been renamed `*.Effectful`.  
+
 ### Improvements to pretty printing and regexes
 
 * In `Text.Pretty`, `Doc` is now a record rather than a type alias. This

GenerateEverything.hs

@@ -117,29 +117,29 @@ sizedTypesModules = map modToFile
   , "Codata.Sized.Cofin.Literals"
   , "Codata.Sized.Colist"
   , "Codata.Sized.Colist.Bisimilarity"
-  , "Codata.Sized.Colist.Categorical"
+  , "Codata.Sized.Colist.Effectful"
   , "Codata.Sized.Colist.Properties"
   , "Codata.Sized.Conat"
   , "Codata.Sized.Conat.Bisimilarity"
   , "Codata.Sized.Conat.Literals"
   , "Codata.Sized.Conat.Properties"
   , "Codata.Sized.Covec"
   , "Codata.Sized.Covec.Bisimilarity"
-  , "Codata.Sized.Covec.Categorical"
+  , "Codata.Sized.Covec.Effectful"
   , "Codata.Sized.Covec.Instances"
   , "Codata.Sized.Covec.Properties"
   , "Codata.Sized.Cowriter"
   , "Codata.Sized.Cowriter.Bisimilarity"
   , "Codata.Sized.Delay"
   , "Codata.Sized.Delay.Bisimilarity"
-  , "Codata.Sized.Delay.Categorical"
+  , "Codata.Sized.Delay.Effectful"
   , "Codata.Sized.Delay.Properties"
   , "Codata.Sized.M"
   , "Codata.Sized.M.Bisimilarity"
   , "Codata.Sized.M.Properties"
   , "Codata.Sized.Stream"
   , "Codata.Sized.Stream.Bisimilarity"
-  , "Codata.Sized.Stream.Categorical"
+  , "Codata.Sized.Stream.Effectful"
   , "Codata.Sized.Stream.Instances"
   , "Codata.Sized.Stream.Properties"
   , "Codata.Sized.Thunk"

README.agda

@@ -64,10 +64,6 @@ module README where
 
 import README.Axiom
 
--- • Category
---     Category theory-inspired idioms used to structure functional
---     programs (functors and monads, for instance).
-
 -- • Codata
 --     Coinductive data types and properties. There are two different
 --     approaches taken. The `Codata.Sized` folder contains the new more
@@ -77,6 +73,10 @@ import README.Axiom
 -- • Data
 --     Data types and properties.
 
+-- • Effect
+--     Category theory-inspired idioms used to structure functional
+--     programs (functors and monads, for instance).
+
 import README.Data
 
 -- • Function
@@ -162,9 +162,9 @@ import Codata.Sized.Colist -- Colists.
 
 -- • Some types used to structure computations
 
-import Category.Functor      -- Functors.
-import Category.Applicative  -- Applicative functors.
-import Category.Monad        -- Monads.
+import Effect.Functor      -- Functors.
+import Effect.Applicative  -- Applicative functors.
+import Effect.Monad        -- Monads.
 
 -- • Equality
 

README/Data.agda

@@ -157,13 +157,13 @@ import Data.Vec.Relation.Unary.All
 import Data.Maybe.Relation.Unary.All
 
 
--- 6. A `Categorical` module/folder that contains categorical
+-- 6. An `Effectful` module/folder that contains effectful
 -- interpretations of the datatype.
 
-import Data.List.Categorical
-import Data.Maybe.Categorical
-import Data.Sum.Categorical.Left
-import Data.Sum.Categorical.Right
+import Data.List.Effectful
+import Data.Maybe.Effectful
+import Data.Sum.Effectful.Left
+import Data.Sum.Effectful.Right
 
 
 -- 7. A `Function` folder that contains lifting of various types of

README/Data/Container/FreeMonad.agda

@@ -9,7 +9,7 @@
 
 module README.Data.Container.FreeMonad where
 
-open import Category.Monad
+open import Effect.Monad
 open import Data.Empty
 open import Data.Unit
 open import Data.Bool.Base using (Bool; true)

src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda

@@ -14,15 +14,15 @@ module Algebra.Lattice.Properties.BooleanAlgebra.Expression
 
 open BooleanAlgebra B
 
-open import Category.Applicative
-import Category.Applicative.Indexed as Applicative
-open import Category.Monad
+open import Effect.Applicative
+import Effect.Applicative.Indexed as Applicative
+open import Effect.Monad
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
-import Data.Vec.Categorical as VecCat
-import Function.Identity.Categorical as IdCat
+import Data.Vec.Effectful as VecCat
+import Function.Identity.Effectful as IdCat
 open import Data.Vec.Properties using (lookup-map)
 open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
   using (Pointwise; ext)

src/Codata/Musical/Colist.agda

@@ -9,7 +9,7 @@
 module Codata.Musical.Colist where
 
 open import Level using (Level)
-open import Category.Monad
+open import Effect.Monad
 open import Codata.Musical.Notation
 open import Codata.Musical.Conat using (Coℕ; zero; suc)
 import Codata.Musical.Colist.Properties

src/Codata/Sized/Colist/Categorical.agda renamed to src/Codata/Sized/Colist/Effectful.agda

@@ -1,17 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Colist
+-- An effectful view of Colist
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Colist.Categorical where
+module Codata.Sized.Colist.Effectful where
 
 open import Codata.Sized.Conat using (infinity)
 open import Codata.Sized.Colist
-open import Category.Functor
-open import Category.Applicative
+open import Effect.Functor
+open import Effect.Applicative
 
 functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Colist A i)
 functor = record { _<$>_ = map }

src/Codata/Sized/Covec/Categorical.agda renamed to src/Codata/Sized/Covec/Effectful.agda

@@ -1,18 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Covec
+-- An effectful view of Covec
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Covec.Categorical where
+module Codata.Sized.Covec.Effectful where
 
 open import Codata.Sized.Conat
 open import Codata.Sized.Covec
-
-open import Category.Functor
-open import Category.Applicative
+open import Effect.Functor
+open import Effect.Applicative
 
 functor : ∀ {ℓ i n} → RawFunctor {ℓ} (λ A → Covec A n i)
 functor = record { _<$>_ = map }

src/Codata/Sized/Covec/Instances.agda

@@ -8,7 +8,7 @@
 
 module Codata.Sized.Covec.Instances where
 
-open import Codata.Sized.Covec.Categorical
+open import Codata.Sized.Covec.Effectful
 
 instance
   covecFunctor = functor