module Kindly.Class where -------------------------------------------------------------------------------- import Control.Category import Data.Kind (Constraint) import Data.Semigroupoid (Semigroupoid (..)) import GHC.Base (Type) -------------------------------------------------------------------------------- -- | A functor @f@ between categories @from@ and @to@ sends objects in -- @Dom f@ to objects in @Cod f@ and morphisms in @Dom f@ to -- morphisms in @Dom f@. -- -- === Laws -- -- [Identity] @'map' 'id' == 'id'@ -- [Composition] @'map' (f . g) == 'map' f . 'map' g@ type CategoricalFunctor :: (from -> to) -> Constraint class (Category (Dom f), Category (Cod f)) => CategoricalFunctor (f :: from -> to) where -- | @Dom f@ is the source category for the functor @f@. type Dom f :: from -> from -> Type -- | @Cod f@ is the target category for the functor @f@. type Cod f :: to -> to -> Type -- | Lift a function of type @Dom f a b@ into a function of type @Cod f (f a) (f b)@. map :: Dom f a b -> Cod f (f a) (f b) type Cat i = i -> i -> Type -- | A Natural Transformation betweeen two functors @f@ and @g@. type Nat :: Cat s -> Cat t -> Cat (s -> t) newtype Nat source target f g where Nat :: (forall x. target (f x) (g x)) -> Nat source target f g runNat :: Nat source target f g -> (forall x. target (f x) (g x)) runNat (Nat f) = f infixr 0 ~> type (~>) c1 c2 = Nat c1 c2 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 (c1 ~> c2) where id :: (c1 ~> c2) a a id = Nat id (.) = o type FunctorOf :: Cat from -> Cat to -> (from -> to) -> Constraint class (CategoricalFunctor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f instance (CategoricalFunctor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f -------------------------------------------------------------------------------- -- NOTE: These these classes go from right to left: class (FunctorOf cat1 (->) p) => MapArg1 cat1 p | p -> cat1 where map1 :: (a `cat1` b) -> p a -> p b map1 = map class (FunctorOf cat1 (cat2 ~> (->)) p, forall x. MapArg1 cat2 (p x)) => MapArg2 cat1 cat2 p | p -> cat2 cat2 where map2 :: (a `cat1` b) -> forall x. p a x -> p b x map2 = runNat . map class (FunctorOf cat1 (cat2 ~> cat3 ~> (->)) p, forall x. MapArg2 cat2 cat3 (p x)) => MapArg3 cat1 cat2 cat3 p | p -> cat1 cat2 cat3 where map3 :: (a `cat1` b) -> forall x y. p a x y -> p b x y map3 f = runNat (runNat (map f))