Iceland Jack's categorical functor proposal

monoidal-functors.cabal

@@ -73,6 +73,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,136 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# 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 Data.Bifunctor qualified as Hask
+import Data.Functor qualified as Hask
+import Data.Functor.Contravariant (Op (..), Predicate (..))
+import Data.Functor.Contravariant qualified as Hask
+import Data.Kind (Constraint, Type)
+import Data.Maybe (Maybe (..))
+
+-- import Data.Profunctor 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 Nat :: Cat s -> Cat t -> Cat (s -> t)
+data Nat source target f f' where
+  Nat :: (FunctorOf source target f, FunctorOf source target f') => (forall x. target (f x) (f' x)) -> Nat source target f f'
+
+-- TODO:
+-- instance Category (Nat (->) (->)) where
+--   id :: Nat (->) (->) a a
+--   id = Nat _
+
+type Cat i = i -> i -> Type
+
+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
+
+--------------------------------------------------------------------------------
+
+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
+
+deriving via (FromFunctor []) instance Functor []
+
+deriving via (FromFunctor Maybe) instance Functor Maybe
+
+--------------------------------------------------------------------------------
+
+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
+
+deriving via (FromContra Predicate) instance Functor Predicate
+
+--------------------------------------------------------------------------------
+
+-- TODO:
+-- newtype FromBifunctor f a b = FromBifunctor (f a b)
+
+-- instance (Hask.Bifunctor f) => Functor f where
+--   type Dom f = (->)
+--   type Cod f = (Nat (->) (->))
+
+--   map :: Hask.Bifunctor f => (a -> b) -> Nat (->) (->) (f a) (f b)
+--   map = _
+
+--------------------------------------------------------------------------------
+
+-- TODO:
+-- newtype FromProfunctor f a b = FromProfunctor (f a b)
+
+-- instance (Hask.Profunctor f) => Functor f where
+--   type Dom f = Op
+--   type Cod f = (Nat (->) (->))
+
+--   map :: (Hask.Profunctor f) => Op a b -> Nat (->) (->) (f a) (f b)
+--   map = _
+
+--------------------------------------------------------------------------------
+-- Examples
+
+type EndofunctorOf :: Cat ob -> (ob -> ob) -> Constraint
+type EndofunctorOf cat = FunctorOf cat cat
+
+type Contravariant :: (Type -> Type) -> Constraint
+type Contravariant = FunctorOf Op (->)
+
+type Bifunctor :: (Type -> Type -> Type) -> Constraint
+type Bifunctor = FunctorOf (->) (Nat (->) (->))
+
+type Profunctor :: (Type -> Type -> Type) -> Constraint
+type Profunctor = FunctorOf Op (Nat (->) (->))
+
+type Trifunctor :: (Type -> Type -> Type -> Type) -> Constraint
+type Trifunctor = FunctorOf (->) (Nat (->) (Nat (->) (->)))
+
+fmap' :: (EndofunctorOf (->) f) => (a -> b) -> f a -> f b
+fmap' = map
+
+contramap' :: (Contravariant f) => (a -> b) -> f b -> f a
+contramap' f = map (Op f)
+
+-- bimap' :: forall f a b c d. FunctorOf (->) (Nat (->) (->)) f => (a -> b) -> (c -> d) -> f a c -> f b d
+-- bimap' f g = _
+
+-- dimap' :: FunctorOf Op (Nat (->) (->)) p => (a -> b) -> (c -> d) -> p b c -> p a d
+-- dimap' f g = _