Iceland Jack's categorical functor proposal

monoidal-functors.cabal

@@ -64,6 +64,7 @@ library
     semigroupoids                 >= 6.0.0 && < 6.1,
     these                         >= 1.2 && < 1.3,
     mtl                           >= 2.2.2 && < 2.4,
+    witherable                    >= 0.4.2 && < 0.5,
 
   exposed-modules:
     Control.Category.Tensor
@@ -73,6 +74,7 @@ library
     Data.Bifunctor.Module
     Data.Bifunctor.Monoidal
     Data.Bifunctor.Monoidal.Specialized
+    Data.Functor.Categorical
     Data.Functor.Invariant
     Data.Functor.Module
     Data.Functor.Monoidal

src/Data/Functor/Categorical.hs

@@ -0,0 +1,263 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- | A scratchpad for implementing Iceland Jack and Ed Kmett's
+-- categorical functor ideas.
+--
+-- If possible, this ought to give us a kind generic functor to
+-- replace 'GBifunctor'.
+--
+-- We also ought to be able to use the same tricks to get a kind
+-- generic Monoidal Functor class.
+module Data.Functor.Categorical where
+
+--------------------------------------------------------------------------------
+
+import Control.Category
+import Control.Monad qualified as Hask
+import Data.Bifunctor qualified as Hask
+import Data.Bool (Bool)
+import Data.Either (Either)
+import Data.Functor.Contravariant (Op (..), Predicate (..))
+import Data.Functor.Contravariant qualified as Hask
+import Data.Functor.Identity (Identity)
+import Data.Kind (Constraint, Type)
+import Data.Maybe (Maybe (..))
+import Data.Profunctor qualified as Hask
+import Data.Semigroupoid
+import Witherable qualified as Hask
+
+--------------------------------------------------------------------------------
+
+type Functor :: (from -> to) -> Constraint
+class (Category (Dom f), Category (Cod f)) => Functor (f :: from -> to) where
+  type Dom f :: from -> from -> Type
+  type Cod f :: to -> to -> Type
+
+  map :: Dom f a b -> Cod f (f a) (f b)
+
+type Cat i = i -> i -> Type
+
+type Nat :: Cat s -> Cat t -> Cat (s -> t)
+data Nat source target f f' where
+  Nat :: (forall x. target (f x) (f' x)) -> Nat source target f f'
+
+instance (Semigroupoid c1, Semigroupoid c2) => Semigroupoid (Nat c1 c2) where
+  o :: Nat c1 c2 j k1 -> Nat c1 c2 i j -> Nat c1 c2 i k1
+  Nat c1 `o` Nat c2 = Nat (c1 `o` c2)
+
+instance (Semigroupoid c1, Semigroupoid c2, Category c1, Category c2) => Category (Nat c1 c2) where
+  id :: Nat c1 c2 a a
+  id = Nat id
+
+  (.) = o
+
+type FunctorOf :: Cat from -> Cat to -> (from -> to) -> Constraint
+class (Functor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f
+
+instance (Functor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f
+
+type EndofunctorOf :: Cat ob -> (ob -> ob) -> Constraint
+type EndofunctorOf cat = FunctorOf cat cat
+
+--------------------------------------------------------------------------------
+
+instance Functor [] where
+  type Dom [] = (->)
+  type Cod [] = (->)
+
+  map :: (a -> b) -> [a] -> [b]
+  map = Hask.fmap
+
+--------------------------------------------------------------------------------
+
+newtype FromFunctor f a = FromFunctor (f a)
+  deriving newtype (Hask.Functor)
+
+instance (Hask.Functor f) => Functor (FromFunctor f) where
+  type Dom (FromFunctor f) = (->)
+  type Cod (FromFunctor f) = (->)
+
+  map :: (a -> b) -> FromFunctor f a -> FromFunctor f b
+  map = Hask.fmap
+
+type CovariantFunctor :: (Type -> Type) -> Constraint
+type CovariantFunctor f = FunctorOf (->) (->) f
+
+fmap :: (CovariantFunctor f) => (a -> b) -> f a -> f b
+fmap = map
+
+deriving via (FromFunctor Identity) instance Functor Identity
+
+deriving via (FromFunctor ((,) a)) instance Functor ((,) a)
+
+deriving via (FromFunctor ((->) r)) instance Functor ((->) r)
+
+deriving via (FromFunctor Maybe) instance Functor Maybe
+
+deriving via (FromFunctor (Either e)) instance Functor (Either e)
+
+--------------------------------------------------------------------------------
+
+newtype FromContra f a = FromContra {getContra :: f a}
+  deriving newtype (Hask.Contravariant)
+
+instance (Hask.Contravariant f) => Functor (FromContra f) where
+  type Dom (FromContra f) = Op
+  type Cod (FromContra f) = (->)
+
+  map :: Dom (FromContra f) a b -> Cod (FromContra f) ((FromContra f) a) ((FromContra f) b)
+  map = Hask.contramap . getOp
+
+type Contravariant :: (Type -> Type) -> Constraint
+type Contravariant f = FunctorOf Op (->) f
+
+contramap :: (Contravariant f) => (a -> b) -> f b -> f a
+contramap f = map (Op f)
+
+deriving via (FromContra Predicate) instance Functor Predicate
+
+--------------------------------------------------------------------------------
+
+newtype FromBifunctor f a b = FromBifunctor (f a b)
+  deriving newtype (Hask.Functor, Hask.Bifunctor)
+
+instance (Hask.Bifunctor p, FunctorOf (->) (->) (p x)) => Functor (FromBifunctor p x) where
+  type Dom (FromBifunctor p x) = (->)
+  type Cod (FromBifunctor p x) = (->)
+
+  map :: (a -> b) -> FromBifunctor p x a -> FromBifunctor p x b
+  map f (FromBifunctor pab) = FromBifunctor (map f pab)
+
+instance (Hask.Bifunctor p, forall x. FunctorOf (->) (->) (p x)) => Functor (FromBifunctor p) where
+  type Dom (FromBifunctor p) = (->)
+  type Cod (FromBifunctor p) = (Nat (->) (->))
+
+  map :: (a -> b) -> (Nat (->) (->)) (FromBifunctor p a) (FromBifunctor p b)
+  map f = Nat (\(FromBifunctor pax) -> FromBifunctor (Hask.first f pax))
+
+type Bifunctor :: (Type -> Type -> Type) -> Constraint
+type Bifunctor p = (forall a. FunctorOf (->) (->) (p a), FunctorOf (->) (Nat (->) (->)) p)
+
+first :: forall p a b. (FunctorOf (->) (Nat (->) (->)) p) => (a -> b) -> forall x. p a x -> p b x
+first f = let (Nat f') = map @_ @_ @p f in f'
+
+second :: (CovariantFunctor (p x)) => (a -> b) -> p x a -> p x b
+second = map
+
+bimap :: (Bifunctor p) => (a -> b) -> (c -> d) -> p a c -> p b d
+bimap f g = first f . second g
+
+-- deriving via (FromBifunctor (,)) instance Functor (,)
+
+instance Functor (,) where
+  type Dom (,) = (->)
+  type Cod (,) = Nat (->) (->)
+
+  map :: (a -> b) -> Nat (->) (->) ((,) a) ((,) b)
+  map f = Nat (Hask.first f)
+
+instance Functor Either where
+  type Dom Either = (->)
+  type Cod Either = Nat (->) (->)
+
+  map :: (e -> e1) -> Nat (->) (->) (Either e) (Either e1)
+  map f = Nat (Hask.first f)
+
+--------------------------------------------------------------------------------
+
+newtype FromProfunctor f a b = FromProfunctor (f a b)
+  deriving newtype (Hask.Functor, Hask.Profunctor)
+
+instance (Hask.Profunctor p, FunctorOf (->) (->) (p x)) => Functor (FromProfunctor p x) where
+  type Dom (FromProfunctor p x) = (->)
+  type Cod (FromProfunctor p x) = (->)
+
+  map :: (a -> b) -> Cod (FromProfunctor p x) (FromProfunctor p x a) (FromProfunctor p x b)
+  map f (FromProfunctor pxa) = FromProfunctor (map f pxa)
+
+instance (Hask.Profunctor p) => Functor (FromProfunctor p) where
+  type Dom (FromProfunctor p) = Op
+  type Cod (FromProfunctor p) = (Nat (->) (->))
+
+  map :: Op a b -> Nat (->) (->) ((FromProfunctor p) a) ((FromProfunctor p) b)
+  map (Op f) = Nat (\(FromProfunctor pax) -> FromProfunctor (Hask.lmap f pax))
+
+type Profunctor :: (Type -> Type -> Type) -> Constraint
+type Profunctor p = (FunctorOf Op (Nat (->) (->)) p, forall x. FunctorOf (->) (->) (p x))
+
+lmap :: forall p a b. (Profunctor p) => (a -> b) -> forall x. p b x -> p a x
+lmap f = let (Nat f') = map @_ @_ @p (Op f) in f'
+
+rmap :: (CovariantFunctor (f x)) => (a -> b) -> f x a -> f x b
+rmap = fmap
+
+dimap :: (Profunctor p) => (a -> b) -> (c -> d) -> p b c -> p a d
+dimap f g = lmap f . rmap g
+
+instance Functor (->) where
+  type Dom (->) = Op
+  type Cod (->) = Nat (->) (->)
+
+  map :: Op a b -> Nat (->) (->) ((->) a) ((->) b)
+  map (Op f) = Nat (\g -> g . f)
+
+--------------------------------------------------------------------------------
+
+newtype FromFilterable f a = FromFilterable (f a)
+  deriving newtype (Hask.Functor, Hask.Filterable)
+
+instance (Hask.Filterable f) => Functor (FromFilterable f) where
+  type Dom (FromFilterable f) = (Hask.Star Maybe)
+  type Cod (FromFilterable f) = (->)
+
+  map :: Hask.Star Maybe a b -> FromFilterable f a -> FromFilterable f b
+  map (Hask.Star f) (FromFilterable fa) = FromFilterable (Hask.mapMaybe f fa)
+
+catMaybes :: (Filterable f) => f (Maybe a) -> f a
+catMaybes = map (Hask.Star id)
+
+filter :: (Filterable f) => (a -> Bool) -> f a -> f a
+filter f = map (Hask.Star (\a -> if f a then Just a else Nothing))
+
+type Filterable = FunctorOf (Hask.Star Maybe) (->)
+
+-- NOTE: These instances conflict with our Covariant Functor
+-- instances. Switching from associated types to Multi Parameter type
+-- classes would fix this.
+
+-- deriving via (FromFilterable []) instance Functor []
+
+-- deriving via (FromFilterable Maybe) instance Functor Maybe
+
+--------------------------------------------------------------------------------
+-- TODO:
+
+type Trifunctor :: (Type -> Type -> Type -> Type) -> Constraint
+type Trifunctor = FunctorOf (->) (Nat (->) (Nat (->) (->)))
+
+-- NOTE This gives us `p a x x -> p b x x` in our co-domain:
+instance Functor (,,) where
+  type Dom (,,) = (->)
+  type Cod (,,) = (Nat (->) (Nat (->) (->)))
+
+  map :: (a -> b) -> (Nat (->) (Nat (->) (->))) ((,,) a) ((,,) b)
+  map f = Nat (Nat (\(x, y, z) -> (f x, y, z)))
+
+-- newtype Mealy m s i o = Mealy { runMealy :: s -> i -> m (o, s) }
+--   deriving
+--     (Hask.Functor, Hask.Applicative, Hask.Monad)
+--     via Hask.StateT s (Hask.ReaderT i m)
+
+-- deriving via (FromFunctor (Mealy m s i)) instance (Hask.Functor m) => Functor (Mealy m s i)
+
+-- instance Functor (Mealy m s) where
+--   type Dom (Mealy m s) = Op
+--   type Cod (Mealy m s) = Nat (->) (->)
+
+--   map :: Dom (Mealy m s) a b -> Cod (Mealy m s) (Mealy m s a) (Mealy m s b)
+--   map = _