Temporarily remove evil. Basic recursion schemes work.

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

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 70278e7afaa766a9a15b6541432b72444f2618e64de1d91dfe39d0af0da80aa7
+-- hash: 36f59318e1bb608d49a3bb377e2ef94dfa811ad60fe6aae86f7be7ffd276ec93
 
 name:           monoids-in-the-categoy-of-endofunctors
 version:        0.1.0.0
@@ -26,17 +26,17 @@ source-repository head
 
 library
   exposed-modules:
-      Category.Evil
+      Category
       Category.Good
-      Category.Neutral
       Category.Neutral.Enriched
-      Category.Neutral.NaturalTransformation
+      Category.Subcategory
       Data.Dict
+      Data.Recursive
   other-modules:
       Paths_monoids_in_the_categoy_of_endofunctors
   hs-source-dirs:
       src
-  default-extensions: BlockArguments ConstraintKinds DataKinds FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs MultiParamTypeClasses NoImplicitPrelude ScopedTypeVariables TypeApplications TypeFamilies TypeOperators Safe
+  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
   build-depends:
       base >=4.13 && <5

package.yaml

@@ -21,6 +21,7 @@ default-extensions:
 - GADTs
 - ImportQualifiedPost
 - InstanceSigs
+- LambdaCase
 - MultiParamTypeClasses
 - NoImplicitPrelude
 - ScopedTypeVariables

src/Category.hs

@@ -1,5 +1,7 @@
 {-# LANGUAGE PolyKinds #-}
-module Category.Neutral where
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Category where
 
 import Category.Good qualified as Good
 import Data.Dict (Dict (Dict), (:-) (Sub), (\\))
@@ -17,6 +19,9 @@ class Category cat where
     identity :: cat a a
     compose :: cat b c -> cat a b -> cat a c
 
+(.) :: Category cat => cat b c -> cat a b -> cat a c
+(.) = compose
+
 instance Category (->) where
     identity x = x
     compose f g x = f (g x)
@@ -29,7 +34,7 @@ instance Category (:-) where
 class Category cat => CovariantEndo cat f where
     coendomap :: cat a b -> cat (f a) (f b)
 
-instance Good.Covariant f => CovariantEndo (->) f where
+instance {-# OVERLAPPABLE #-} Good.Covariant f => CovariantEndo (->) f where
     coendomap = Good.comap
 
 -- | A contravariant endofunctor in an unenriched category.
@@ -149,3 +154,19 @@ class Applicative cat m => Monad cat m where
 
 instance Good.Monad m => Monad (->) m where
     join = Good.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
+    identity = Nat identity
+    compose (Nat f) (Nat g) = Nat (compose f g)
+
+class AnyC a
+instance AnyC a
+
+class AnyC2 a b
+instance AnyC2 a b

src/Category/Evil.hs

@@ -1,70 +0,0 @@
-{-# LANGUAGE PolyKinds #-}
-module Category.Evil where
-
-import Category.Good qualified as Good
-import Category.Neutral qualified as Neutral
-import Data.Dict (Dict (Dict), (:-) (Sub))
-import Data.Kind (Constraint, Type)
-
-class Category (hom :: i -> i -> Type) (obj :: i -> Constraint) where
-    identity :: obj a => proxy obj -> hom a a
-    compose :: (obj a, obj b, obj c) => proxy obj -> hom b c -> hom a b -> hom a c
-
-instance Neutral.Category hom => Category hom obj where
-    identity _ = Neutral.identity
-    compose _ = Neutral.compose
-
-class MonoidalObjects k where
-    type Unit obj :: k
-    type Product obj :: k -> k -> k
-
-instance MonoidalObjects Type where
-    type Unit Type = ()
-    type Product Type = (,)
-
-class MonoidalObjects i => ContainsMonoidalObjects (obj :: i -> Constraint) where
-    monObjUnit :: Dict (obj (Unit i))
-    monObjFactor :: (obj a, obj b) => Dict (obj (Product i a b))
-    monObjDistribute :: obj (Product i a b) => Dict (obj a, obj b)
-
-class (Category hom obj, ContainsMonoidalObjects obj) => Monoidal hom (obj :: i -> Constraint) where
-    --monBi :: proxy cat -> Dict (BiEndo cat (Product cat))
-    monIdLI :: obj a => proxy obj -> a `hom` Product i a (Unit i)
-    monIdRI :: obj a => proxy obj -> a `hom` Product i (Unit i) a
-    monIdLE :: obj a => proxy obj -> Product i a (Unit i) `hom` a
-    monIdRE :: obj a => proxy obj -> Product i (Unit i) a `hom` a
-    monAssocL :: (obj a, obj b, obj c) => proxy obj -> Product i (Product i a b) c `hom` Product i a (Product i b c)
-    monAssocR :: (obj a, obj b, obj c) => proxy obj -> Product i a (Product i b c) `hom` Product i (Product i a b) c
-
-instance (Neutral.Monoidal hom, ContainsMonoidalObjects obj, Neutral.Unit hom ~ Unit i, Neutral.Product hom ~ Product i) => Monoidal hom (obj :: i -> Constraint) where
-    monIdLI _ = Neutral.monIdLI
-    monIdRI _ = Neutral.monIdRI
-    monIdLE _ = Neutral.monIdLE
-    monIdRE _ = Neutral.monIdRE
-    monAssocL _ = Neutral.monAssocL
-    monAssocR _ = Neutral.monAssocR
-
-class Category hom obj => Endofunctor hom obj f where
-    endomapObj :: obj a => proxy hom -> Dict (obj (f a))
-
-class Endofunctor hom obj f => CovariantEndo hom obj f where
-    coendomap :: (obj a, obj b) => proxy obj -> hom a b -> hom (f a) (f b)
-
-instance (Endofunctor hom obj f, Neutral.CovariantEndo hom f) => CovariantEndo hom obj f where
-    coendomap _ = Neutral.coendomap
-
-class (Category domHom domObj, Category codHom codObj) => Functor domHom domObj codHom codObj f where
-    mapObj :: domObj a => proxy domHom -> proxy' domObj -> proxy'' codHom -> Dict (codObj (f a))
-
-instance Endofunctor hom obj f => Functor hom obj hom obj f where
-    mapObj _ _ = endomapObj
-
-class Functor domHom domObj codHom codObj f => Covariant domHom domObj codHom codObj f where
-    comap :: (domObj a, domObj b) => proxy domObj -> proxy' codObj -> domHom a b -> codHom (f a) (f b)
-
-instance (Functor domHom domObj codHom codObj f, Neutral.Covariant domHom codHom f) => Covariant domHom domObj codHom codObj f where
-    comap _ _ = Neutral.comap
-
-class (Monoidal domHom domObj, Monoidal codHom codObj, Covariant domHom domObj codHom codObj f) => Applicative domHom domObj codHom codObj (f :: i -> j) where
-    unit :: proxy domHom -> proxy' domObj -> proxy'' codHom -> proxy''' codObj -> codHom (Unit j) (f (Unit i))
-    zip :: proxy domHom -> proxy' domObj -> proxy'' codObj -> codHom (Product j (f a) (f b)) (f (Product i a b))

src/Category/Neutral/Enriched.hs

@@ -1,11 +0,0 @@
-module Category.Neutral.Enriched where
-
-import Category.Neutral qualified as Neutral
-
-class Neutral.Monoidal under => Category under cat where
-    identity :: Neutral.Unit under `under` cat a a
-    compose :: Neutral.Product under (cat b c) (cat a b) `under` cat a c
-
-instance Neutral.Category cat => Category (->) cat where
-    identity () = Neutral.identity
-    compose (f, g) = Neutral.compose f g

src/Category/Neutral/NaturalTransformation.hs

@@ -1,20 +0,0 @@
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE UndecidableInstances #-}
-module Category.Neutral.NaturalTransformation where
-
-import Category.Neutral
-import Data.Kind (Type)
-
--- f , g :: i -> j
--- (~>) :: j -> j -> Type
--- Nat :: (i -> j) -> (i -> j) -> Type
-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
-    identity = Nat identity
-    compose (Nat f) (Nat g) = Nat (compose f g)

src/Data/Recursive.hs

@@ -0,0 +1,84 @@
+{-# 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
+    project :: cat t (Base t t)
+
+class (Category cat, CovariantEndo 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
+
+data Fin (n :: N) where
+    FZ :: Fin ('S n)
+    FS :: Fin n -> Fin ('S n)
+
+data FinF (r :: N -> Type) (n :: N) :: Type where
+    FZF :: FinF r ('S n)
+    FSF :: r n -> FinF r ('S n)
+
+type instance Base Fin = FinF
+
+instance CovariantEndo Nat FinF where
+    coendomap (Nat f) = Nat \case
+        FZF -> FZF
+        (FSF r) -> FSF (f r)
+
+instance Recursive Nat Fin where
+    project = Nat \case
+        FZ -> FZF
+        (FS n) -> FSF n
+
+data Vec (a :: Type) (n :: N) :: Type where
+    VZ :: Vec a 'Z
+    VS :: a -> Vec a n -> Vec a ('S n)
+
+data VecF (a :: Type) (r :: N -> Type) (n :: N) :: Type where
+    VZF :: VecF a r 'Z
+    VSF :: a -> r n -> VecF a r ('S n)
+
+type instance Base (Vec a) = VecF a
+
+instance CovariantEndo Nat (VecF a) where
+    coendomap (Nat f) = Nat \case
+        VZF -> VZF
+        (VSF x r) -> VSF x (f r)
+
+instance Recursive Nat (Vec a) where
+    project = Nat \case
+        VZ -> VZF
+        (VS x r) -> VSF x r
+
+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
+
+newtype Ixr a n = Ixr { getIxr :: Vec a n -> a }
+
+indexer :: Fin ~> Ixr a
+indexer = cata (Nat alg)
+    where alg :: FinF (Ixr a) n -> Ixr a n
+          alg = \case
+                  FZF -> Ixr (\case (VS x _) -> x)
+                  (FSF (Ixr r)) -> Ixr (\case (VS _ xs) -> r xs)
+
+index :: Vec a n -> Fin n -> a
+index xs i = getIxr (runNat indexer i) xs