Moved Category to Effect: issue #1636

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

src/Codata/Sized/Delay/Categorical.agda → src/Codata/Sized/Delay/Effectful.agda

@@ -1,18 +1,18 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Delay
+-- An effectful view of Delay
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Delay.Categorical where
+module Codata.Sized.Delay.Effectful where
 
 open import Codata.Sized.Delay
 open import Function
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Data.These using (leftMost)
 
 functor : ∀ {i ℓ} → RawFunctor {ℓ} (λ A → Delay A i)

src/Codata/Sized/Stream/Categorical.agda → src/Codata/Sized/Stream/Effectful.agda

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

src/Codata/Sized/Stream/Instances.agda

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

src/Data/Container/FreeMonad.agda

@@ -14,7 +14,7 @@ open import Data.Product
 open import Data.Container
 open import Data.Container.Combinator using (const; _⊎_)
 open import Data.W using (sup)
-open import Category.Monad
+open import Effect.Monad
 
 infixl 1 _⋆C_
 infix  1 _⋆_

src/Data/Container/Indexed/FreeMonad.agda

@@ -10,7 +10,7 @@ module Data.Container.Indexed.FreeMonad where
 
 open import Level
 open import Function hiding (const)
-open import Category.Monad.Predicate
+open import Effect.Monad.Predicate
 open import Data.Container.Indexed
 open import Data.Container.Indexed.Combinator hiding (id; _∘_)
 open import Data.Empty

src/Data/Fin/Properties.agda

@@ -11,8 +11,8 @@ module Data.Fin.Properties where
 
 open import Axiom.Extensionality.Propositional
 open import Algebra.Definitions using (Involutive)
-open import Category.Applicative using (RawApplicative)
-open import Category.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Functor using (RawFunctor)
 open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
@@ -938,7 +938,7 @@ pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
   punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
 
 ------------------------------------------------------------------------
--- Categorical
+-- Effectful
 ------------------------------------------------------------------------
 
 module _ {f} {F : Set f → Set f} (RA : RawApplicative F) where

src/Data/Fin/Substitution/Lemmas.agda

@@ -8,7 +8,7 @@
 
 module Data.Fin.Substitution.Lemmas where
 
-import Category.Applicative.Indexed as Applicative
+import Effect.Applicative.Indexed as Applicative
 open import Data.Fin.Substitution
 open import Data.Nat hiding (_⊔_; _/_)
 open import Data.Fin.Base using (Fin; zero; suc; lift)

src/Data/List/Categorical.agda → src/Data/List/Effectful.agda

@@ -1,19 +1,19 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of List
+-- An effectful view of List
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.Categorical where
+module Data.List.Effectful where
 
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
 open import Data.Bool.Base using (false; true)
 open import Data.List.Base
 open import Data.List.Properties
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Function
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; refl)

src/Data/List/Instances.agda

@@ -9,7 +9,7 @@
 module Data.List.Instances where
 
 open import Data.List.Base
-open import Data.List.Categorical
+open import Data.List.Effectful
 open import Data.List.Properties
   using (≡-dec)
 open import Data.List.Relation.Binary.Pointwise

src/Data/List/Membership/Propositional/Properties.agda

@@ -9,7 +9,7 @@
 module Data.List.Membership.Propositional.Properties where
 
 open import Algebra using (Op₂; Selective)
-open import Category.Monad using (RawMonad)
+open import Effect.Monad using (RawMonad)
 open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
@@ -19,7 +19,7 @@ open import Data.List.Membership.Propositional
 import Data.List.Membership.Setoid.Properties as Membershipₛ
 open import Data.List.Relation.Binary.Equality.Propositional
   using (_≋_; ≡⇒≋; ≋⇒≡)
-open import Data.List.Categorical using (monad)
+open import Data.List.Effectful using (monad)
 open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_)
 open import Data.Nat.Properties
 open import Data.Product hiding (map)

src/Data/List/NonEmpty.agda

@@ -9,7 +9,7 @@
 module Data.List.NonEmpty where
 
 open import Level using (Level)
-open import Category.Monad
+open import Effect.Monad
 open import Data.Bool.Base using (Bool; false; true; not; T)
 open import Data.Bool.Properties
 open import Data.List.Base as List using (List; []; _∷_)

src/Data/List/NonEmpty/Categorical.agda → src/Data/List/NonEmpty/Effectful.agda

@@ -1,21 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of List⁺
+-- An effectful view of List⁺
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.NonEmpty.Categorical where
+module Data.List.NonEmpty.Effectful where
 
 open import Agda.Builtin.List
-import Data.List.Categorical as List
+import Data.List.Effectful as List
 open import Data.List.NonEmpty
 open import Data.Product using (uncurry)
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-open import Category.Comonad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
+open import Effect.Comonad
 open import Function
 
 ------------------------------------------------------------------------