Working on improving documentation.

.editorconfig

@@ -6,3 +6,6 @@ indent_style = space
 indent_size = 4
 trim_trailing_whitespace = true
 insert_final_newline = true
+
+[*.yml]
+indent_size = 2

README.md

@@ -1,34 +1,15 @@
-# monoids-in-the-categoy-of-endofunctors
+# Monoids in the Category of Endofunctors
+This is a **toy** library for studying the field of [Abstract Nonsense](https://en.wikipedia.org/wiki/Abstract_nonsense) through Haskell.
+I would fire anyone who tried to do any of this crap in production.
 
-Abstract nonsense in Haskell: category theory, recursion schemes, dependent data types, etc.
-The current version only contains category theory.
+This library currently includes:
+* Category theory (`Category`)
+* Recursion schemes (`Category.Functor.Foldable`)
+* Dependent types, type-level programming, and codata (`Data`)
+* Dependent quantifiers (as a typeclass; `Quantifier`)
 
-## Category theory morality
-Each morality level re-defines the typeclasses of the level before it in a more general way.
-This generality comes at the cost of the typeclasses being more difficult to understand and use, which is why the excessively general, incomprehensible, and virtually unusable stuff is called 'evil'.
+For further information, build and read the Haddock.
 
-### Good
-The 'good' alignment contains more-or-less standard Haskell that any Haskeller should be able to understand.
-It works exclusively in the category of types.
-
-### Neutral
-The 'neutral' alignment is more abstract, and allows working with categories other than Type.
-This generalization lets us speak of functors which are not endofunctors, the category of constraints or equality, etc..
-
-In this case a category is defined by a hom, and its objects are any value of the type the hom operates on.
-(This is perhaps a confusing wording; as an example, the category defined by `->` has *all* types as objects.)
-
-Here's some stuff we can talk about in neutral but not good:
-* Categories, monoidal categories, and enriched categories.
-* Functors which are not endofunctors (such as `:-`).
-* Natural transformations.
-* Monoids in categories other than Type.
-
-### Evil
-The 'evil' alignment generalizes categories to be defined both by a hom *and* a constraint restricting its objects.
-This broadens what we are allowed to do a *lot*, but Haskell is *really* not meant to be used in this way,
-making actually *doing* these things and using the resultant APIs extremely difficult.
-
-Here are some new things we can describe in evil:
-* `Set` can now finally get a functor instance: it is an endofunctor in the category of ordered types.
-* Monads are directly defined as monoid objects in the monoidal category of endofunctors, rather than as their own special typeclass. (Monad is still available as a convenient alias.)
+## Content warning
+This library is an abuse of GHC Haskell and an abuse of common sense.
+Do not attempt to view this library if you are faint of heart.

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

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: cd92b699ef3ea167b65a8294cb6f08cb475d5aba3d96aeb8b85abfb4e90daf99
+-- hash: 09f2a99c2b84f61ffd46f9cbdb6958c3b1ac66bc38e80f8b92e02d5fa0813490
 
 name:           monoids-in-the-category-of-endofunctors
 version:        0.1.0.0
@@ -46,7 +46,7 @@ library
       Paths_monoids_in_the_category_of_endofunctors
   hs-source-dirs:
       src
-  default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures EmptyCase FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
+  default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures EmptyCase FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PatternSynonyms PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators ViewPatterns
   ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-missing-safe-haskell-mode -Wno-safe -Wno-unsafe
   build-depends:
       base >=4.13 && <5

package.yaml

@@ -26,6 +26,7 @@ default-extensions:
 - LambdaCase
 - MultiParamTypeClasses
 - NoImplicitPrelude
+- PatternSynonyms
 - PolyKinds
 - QuantifiedConstraints
 - RankNTypes
@@ -33,6 +34,7 @@ default-extensions:
 - TypeApplications
 - TypeFamilies
 - TypeOperators
+- ViewPatterns
 
 ghc-options:
 - -Weverything

src/Category.hs

@@ -1,3 +1,9 @@
+-- | A category theory prelude which re-exports other modules.
+-- Please refer to their respective haddocks.
+--
+-- This does not export *every* category module;
+-- only those which are likely to be relevant to every program.
+-- For example, "Category.Functor.Foldable" is not included here.
 module Category
     ( module Category.Base
     , module Category.Constraint

src/Category/Base.hs

@@ -3,18 +3,17 @@ module Category.Base where
 import Data.Dict (Dict (Dict))
 import Data.Kind (Constraint, Type)
 
+-- | A typeclass which is implemented for everything.
 class Vacuous (a :: i)
 instance Vacuous (a :: i)
 
-class Bottom (a :: i) where
-    bottom :: forall b proxy. proxy a -> b
-
 class Semigroupoid (q :: i -> i -> Type) where
     type Obj q :: i -> Constraint
     type Obj _ = Vacuous
     observe :: a `q` b -> Dict (Obj q a, Obj q b)
     default observe :: Obj q ~ Vacuous => a `q` b -> Dict (Obj q a, Obj q b)
     observe _ = Dict
+    -- | Associative composition of morphisms.
     (.) :: b `q` c -> a `q` b -> a `q` c
 
 instance Semigroupoid (->) where

src/Category/Functor/Foldable/TH.hs

@@ -1,6 +1,11 @@
-{-# LANGUAGE TemplateHaskell #-}
+-- | This module is incomplete and buggy! Do not use it!
 module Category.Functor.Foldable.TH where
 
+--
+-- This code was my first time writing template Haskell.
+-- It was shoddily thrown together and is in severe need of a rewrite.
+--
+
 import Data.Char (GeneralCategory (..), generalCategory)
 import Data.Maybe (fromMaybe, isNothing)
 import Language.Haskell.TH

src/Category/Monoidal.hs

@@ -1,3 +1,4 @@
+-- | Monoidal categories.
 module Category.Monoidal where
 
 import Category.Base
@@ -6,16 +7,28 @@ import Category.Functor
 import Data.Either (Either (Left, Right))
 import Data.Void (Void, absurd)
 
+-- | A category is monoidal if it has a product and a unit for that product.
+-- A category can have multiple tensor products and be monoidal in multiple ways,
+-- including the category of types itself,
+-- so instead of using a @Monoidal@ typeclass, we use a @TensorProduct@ typeclass.
 class Bifunctor f => TensorProduct (f :: i -> i -> i) where
+    -- | The identity object of the product.
     type Unit f :: i
+    -- | The identity object is actually an object in the category.
     unitObj :: proxy f -> Dict (Obj (Dom f) (Unit f))
 
+    -- | 'Unit' is the identity of the product; introduce a value on the left of a product.
     unitLI  :: Dom f a (f a (Unit f))
+    -- | 'Unit' is the identity of the product; introduce a value on the right of a product.
     unitRI  :: Dom f a (f (Unit f) a)
+    -- | 'Unit' is the identity of the product; eliminate a product, projecting a value on the right.
     unitLE  :: Dom f (f a (Unit f)) a
+    -- | 'Unit' is the identity of the product; eliminate a product, projecting a value on the left.
     unitRE  :: Dom f (f (Unit f) a) a
 
+    -- | The product is associative; associate to the left.
     assocL  :: Dom f (f a (f b c)) (f (f a b) c)
+    -- | The product is associative; associate to the right.
     assocR  :: Dom f (f (f a b) c) (f a (f b c))
 
 instance TensorProduct (,) where

src/Category/Unit.hs

@@ -1,7 +1,9 @@
+-- | The 'Unit' category contains exactly one object and one morphism.
 module Category.Unit where
 
 import Category.Base
 
+-- | A category with exactly one morphism.
 data Unit (a :: ()) (b :: ()) = Unit
 
 instance Semigroupoid Unit where

src/Category/Void.hs

@@ -1,12 +1,20 @@
+-- | The `Void` category contains no objects and no morphisms.
 module Category.Void where
 
 import Category.Base
 import Data.Proxy
-import Data.Void qualified as V
 
-data Void (a :: V.Void) (b :: V.Void)
+-- | The type of no morphisms.
+data Void (a :: i) (b :: i)
+
+-- | A typeclass which is not implemented for anything.
+-- It's possible to write an implementation for this because Haskell isn't total,
+-- but you really, really shouldn't.
+class Bottom (a :: i) where
+    bottom :: forall b proxy. proxy a -> b
 
 instance Semigroupoid Void where
+    -- No values are objects.
     type Obj Void = Bottom
     observe = \case {}
     (.) = \case {}

src/Data/Dict.hs

@@ -1,4 +1,7 @@
 module Data.Dict where
 
+-- | Constraint instances can be stored as values with GADTs.
 data Dict c where
+    -- | You can only use this type constructor if an instance of @c@ is in scope;
+    -- pattern matching against it brings an instance of @c@ into scope.
     Dict :: c => Dict c

src/Data/Nat.hs

@@ -1,3 +1,4 @@
+-- | The natural numbers and associated types and functions.
 module Data.Nat where
 
 import Category
@@ -6,8 +7,11 @@ import Data.Kind (Type)
 import Data.Maybe (Maybe (Nothing, Just))
 import Quantifier
 
-data N = Z | S N
+-- | The (co-)natural numbers.
+data N = Z   -- ^ Zero
+       | S N -- ^ Successor (@+1@)
 
+-- | Infinity, represented as the fixpoint of the successor function.
 inf :: N
 inf = S inf
 
@@ -18,17 +22,19 @@ instance Pi N where
     depi ZTy = Z
     depi (STy n) = S (depi n)
 
+-- | Disregard this and use @'TyC' N@ instead.
 class NTyC n where
-    nTy :: Ty N n
+    depic_n :: Ty N n
 instance NTyC 'Z where
-    nTy = ZTy
+    depic_n = ZTy
 instance NTyC n => NTyC ('S n) where
-    nTy = STy nTy
+    depic_n = STy depic_n
 
 instance PiC N where
     type TyC N = NTyC
-    depic = nTy
+    depic = depic_n
 
+-- | The base functor for @'Ty' N@.
 data NTyF r n where
     ZTyF :: NTyF r 'Z
     STyF :: r n -> NTyF r ('S n)
@@ -68,14 +74,18 @@ instance Corecursive (Ty N) where
         ZTyF -> ZTy
         (STyF r) -> STy r
 
+-- | Type-level addition.
 type family (:+) (m :: N) (n :: N) :: N where
     'Z   :+ n =          n
     'S m :+ n = 'S (m :+ n)
 
+-- | A proof that the successor function is injective.
 injective :: forall m n. Ty N m -> ('S m ~ 'S n) :- (m ~ n)
 injective ZTy = Sub Dict
 injective (STy i) = case injective i of Sub Dict -> Sub Dict
 
+-- | A proof that zero is the right identity of addition.
+-- (The constraint solver can prove the left identity on its own.)
 rightZero :: forall m. Ty N m -> Dict ((m :+ 'Z) ~ m)
 rightZero ZTy = Dict
 rightZero (STy i) = case rightZero i of Dict -> Dict

src/Data/Proxy.hs

@@ -1,4 +1,15 @@
+-- | GHC's @TypeApplications@ extension is a poor choice for explicit type arguments
+-- because the order of arguments can (and does) vary between GHC versions,
+-- and doesn't let you control which arguments are implicit and which are explicit.
+--
+-- 'Proxy' provides a better alternative for passing explicit type arguments.
 module Data.Proxy where
 
+-- | A type family of singletons used for explicit type arguments without TypeApplications.
 data Proxy (a :: i) where
+    -- | You can specify the type used with @Proxy :: Proxy a@,
+    -- or @Proxy \@a@ using TypeApplications.
+    --
+    -- Why even bother with the proxy if I'm going to recommend TypeApplications anyway?
+    -- Because you get explicit control of argument order, and don't /require/ TypeApplications.
     Proxy :: Proxy a

src/Quantifier.hs

@@ -1,17 +1,50 @@
+{-# LANGUAGE UndecidableInstances #-}
+-- | Dependent quantification is when a function can use the function's argument
+-- both in to compute the result and as part of a type signature.
+--
+-- Consider this function:
+--
+-- > replicate :: forall a. pi (n :: Nat) -> a -> Vec a n`
+-- > replicate (S n) x = x : replicate n x
+--
+-- The argument @n@ determines both the type of the result (@Vec a n@)
+-- and the number of times @x@ is replicated (via recursion).
+--
+-- GHC Haskell does not currently natively support dependent types,
+-- so instead we have to approximate them through "singletons"
+-- (not to be confused with the singleton pattern from OOP).
+--
+-- The purpose of this module is to add a typeclass for singletons
+-- to make approximating dependent quantifiers in Haskell
+-- more consistent and general.
+--
+-- Unfortunately, the techique used here requires a lot of boilerplate,
+-- but it's the best option we currently have.
+--
+-- This technique was first described in [Conor McBride's Hasochism paper](https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf);
+-- the idea to make a `Pi` typeclass was my own, but I'm sure it's been done before.
 module Quantifier where
 
 import Data.Kind (Constraint, Type)
 import Data.Maybe (Maybe (Nothing, Just))
 
--- | An explicit dependent quantifier.
+-- | A typeclass faciliating explicit dependent quantifiers.
 class Pi (ty :: Type) where
+    -- | The type family @`Ty` ty :: ty -> `Type`@ is isomorphic to @ty@,
+    -- with each value @x :: ty@ corresponding with a singleton type @`Ty` ty x@.
     data Ty ty :: ty -> Type
-    depi :: forall a. Ty ty a -> ty
+    -- | Takes the unique value of @'Ty' ty x@ and returns the corresponding value of @x@ in @ty@.
+    depi :: forall x. Ty ty x -> ty
 
--- | An implicit dependent quantifier.
+-- | A typeclass faciliating implicit dependent quantifiers.
 class Pi ty => PiC (ty :: Type) where
+    -- | Because @'Ty' ty x@ has a unique value, we can define a typeclass @'TyC' ty x@
+    -- with a unique instances which gives us that unique value.
+    -- Thus, if the type inference system can infer the value of @x@ on the type level,
+    -- we can get @x@ on the value level as well.
     type TyC ty :: ty -> Constraint
-    depic :: forall a. TyC ty a => Ty ty a
+    -- | Get the unique value of the singleton type @'Ty' ty x@.
+    depic :: forall x. TyC ty x => Ty ty x
 
 instance Pi a => Pi (Maybe a) where
     data Ty (Maybe a) :: Maybe a -> Type where
@@ -19,3 +52,18 @@ instance Pi a => Pi (Maybe a) where
         JustTy :: Ty a x -> Ty (Maybe a) ('Just x)
     depi NothingTy = Nothing
     depi (JustTy x) = Just (depi x)
+
+-- | The typeclass @'TyC' ('Maybe' a)@, which must be defined as its own typeclass
+-- because associated typeclasses aren't a thing.
+class MaybeTyC (x :: Maybe a) where
+    depic_maybe :: Ty (Maybe a) x
+
+instance MaybeTyC 'Nothing where
+    depic_maybe = NothingTy
+
+instance (PiC a, TyC a x) => MaybeTyC ('Just x) where
+    depic_maybe = JustTy depic
+
+instance PiC a => PiC (Maybe a) where
+    type TyC (Maybe a) = MaybeTyC
+    depic = depic_maybe