introduce Yoneda, drop Dual

categories.cabal

@@ -27,7 +27,6 @@ library
 
   exposed-modules:
     Math.Category
-    Math.Category.Dual
     Math.Category.Product
     Math.Category.Sum
     Math.Functor

src/Math/Category.hs

@@ -9,12 +9,24 @@
 
 module Math.Category 
   ( Category(..)
+  , Yoneda(..)
+  , Op
   , Vacuous
   ) where
 
 import Data.Constraint    as Constraint
 import Data.Type.Equality as Equality
 import Data.Type.Coercion as Coercion
+import qualified Prelude
+
+-- | The <http://ncatlab.org/nlab/show/Yoneda+embedding Yoneda embedding>.
+--
+-- Yoneda_C :: C -> [ C^op, Set ]
+newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a }
+
+type family Op (p :: i -> i -> *) :: i -> i -> * where
+  Op (Yoneda p) = p
+  Op p = Yoneda p
 
 class Vacuous (a :: i)
 instance Vacuous a
@@ -34,6 +46,14 @@ class Category (p :: i -> i -> *) where
   default target :: (Ob p ~ Vacuous) => p a b -> Dict (Ob p b)
   target _ = Dict
 
+  unop :: Op p b a -> p a b
+  default unop :: Op p ~ Yoneda p => Op p b a -> p a b
+  unop = getOp
+
+  op :: p b a -> Op p a b
+  default op :: Op p ~ Yoneda p => p b a -> Op p a b
+  op = Op
+
 instance Category (->) where
   id = Prelude.id
   (.) = (Prelude..)
@@ -49,3 +69,12 @@ instance Category (:~:) where
 instance Category Coercion where
   id = Coercion
   (.) = Prelude.flip Coercion.trans
+
+instance (Category p, Op p ~ Yoneda p) => Category (Yoneda p) where
+  type Ob (Yoneda p) = Ob p
+  id = Op id
+  Op f . Op g = Op (g . f)
+  source (Op f) = target f
+  target (Op f) = source f
+  unop = Op
+  op = getOp

src/Math/Functor.hs

@@ -11,40 +11,41 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Math.Functor 
   ( Functor(..)
   , FunctorOf
   , Nat(..)
+  , Bifunctor, Dom2, Cod2
+  , bimap, first, second
+  , dimap
+  , contramap
   ) where
 
 import Data.Constraint as Constraint
 import Data.Type.Equality as Equality
 import Data.Type.Coercion as Coercion
 import Math.Category
-import Math.Category.Dual
-import Prelude (($))
+import Prelude (($), Either(..))
+
+--------------------------------------------------------------------------------
+-- * Functors
+--------------------------------------------------------------------------------
 
 class (Category (Cod f), Category (Dom f)) => Functor (f :: i -> j) where
   type Dom f :: i -> i -> *
   type Cod f :: j -> j -> *
   fmap :: Dom f a b -> Cod f (f a) (f b)
 
-instance Functor (->) where
-  type Dom (->) = Dual (->)
-  type Cod (->) = Nat (->) (->)
-  fmap (Dual f) = Nat (. f)
+contramap :: Functor f => Op (Dom f) b a -> Cod f (f a) (f b)
+contramap = fmap . unop
 
 instance Functor ((->) e) where
   type Dom ((->) e) = (->)
   type Cod ((->) e) = (->)
   fmap = (.)
 
-instance Functor (:-) where
-  type Dom (:-) = Dual (:-)
-  type Cod (:-) = Nat (:-) (->)
-  fmap (Dual f) = Nat (. f)
-
 instance Functor ((:-) e) where
   type Dom ((:-) e) = (:-)
   type Cod ((:-) e) = (->)
@@ -56,33 +57,38 @@ instance Functor Dict where
   fmap p Dict = case p of
     Sub q -> q
 
-instance Functor (:~:) where
-  type Dom (:~:) = Dual (:~:)
-  type Cod (:~:) = Nat (:~:) (->)
-  fmap (Dual f) = Nat (. f)
-
 instance Functor ((:~:) e) where
   type Dom ((:~:) e) = (:~:)
   type Cod ((:~:) e) = (->)
   fmap = (.)
 
-instance Functor Coercion where
-  type Dom Coercion = Dual Coercion
-  type Cod Coercion = Nat Coercion (->)
-  fmap (Dual f) = Nat (. f)
-
 instance Functor (Coercion e) where
   type Dom (Coercion e) = Coercion
   type Cod (Coercion e) = (->)
   fmap = (.)
 
+instance Functor ((,) e) where
+  type Dom ((,) e) = (->)
+  type Cod ((,) e) = (->)
+  fmap f ~(a,b) = (a, f b)
+
+instance Functor (Either a) where
+  type Dom (Either a) = (->)
+  type Cod (Either a) = (->)
+  fmap _ (Left a) = Left a
+  fmap f (Right b) = Right (f b)
+
 class (Dom f ~ c, Cod f ~ d, Functor f) => FunctorOf (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j)
 instance (Dom f ~ c, Cod f ~ d, Functor f) => FunctorOf c d f 
 
 ob :: forall f a. Functor f => Ob (Dom f) a :- Ob (Cod f) (f a)
 ob = Sub $ case source (fmap (id :: Dom f a a) :: Cod f (f a) (f a)) of
   Dict -> Dict
 
+--------------------------------------------------------------------------------
+-- * Natural Transformations
+--------------------------------------------------------------------------------
+
 data Nat (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j) (g :: i -> j) where
   Nat :: (FunctorOf c d f, FunctorOf c d g) => { runNat :: forall a. Ob c a => d (f a) (g a) }  -> Nat c d f g
 
@@ -96,9 +102,9 @@ instance (Category c, Category d) => Category (Nat c d) where
   target Nat{} = Dict
 
 instance (Category c, Category d) => Functor (Nat c d) where
-  type Dom (Nat c d) = Dual (Nat c d)
+  type Dom (Nat c d) = Op (Nat c d)
   type Cod (Nat c d) = Nat (Nat c d) (->)
-  fmap (Dual f) = Nat (. f)
+  fmap (Op f) = Nat (. f)
 
 instance (Category c, Category d) => Functor (Nat c d f) where
   type Dom (Nat c d f) = Nat c d
@@ -110,5 +116,64 @@ instance (Category c, Category d) => Functor (FunctorOf c d) where
   type Cod (FunctorOf c d) = (:-)
   fmap Nat{} = Sub Dict
 
+instance Functor (->) where
+  type Dom (->) = Op (->)
+  type Cod (->) = Nat (->) (->)
+  fmap (Op f) = Nat (. f)
+
+instance Functor (:-) where
+  type Dom (:-) = Op (:-)
+  type Cod (:-) = Nat (:-) (->)
+  fmap (Op f) = Nat (. f)
+
+instance Functor (:~:) where
+  type Dom (:~:) = Op (:~:)
+  type Cod (:~:) = Nat (:~:) (->)
+  fmap (Op f) = Nat (. f)
+
+instance Functor Coercion where
+  type Dom Coercion = Op Coercion
+  type Cod Coercion = Nat Coercion (->)
+  fmap (Op f) = Nat (. f)
+
+instance Functor (,) where
+  type Dom (,) = (->)
+  type Cod (,) = Nat (->) (->)
+  fmap f = Nat $ \(a,b) -> (f a, b)
+
+instance Functor Either where
+  type Dom Either = (->)
+  type Cod Either = Nat (->) (->)
+  fmap f0 = Nat (go f0) where
+    go :: (a -> b) -> Either a c -> Either b c
+    go f (Left a)  = Left (f a)
+    go _ (Right b) = Right b
+
+--------------------------------------------------------------------------------
+-- * Bifunctors
+--------------------------------------------------------------------------------
+
+type family NatDom (f :: (i -> j) -> (i -> j) -> *) :: (i -> i -> *) where NatDom (Nat p q) = p
+type family NatCod (f :: (i -> j) -> (i -> j) -> *) :: (j -> j -> *) where NatCod (Nat p q) = q
+
+type Dom2 p = NatDom (Cod p)
+type Cod2 p = NatCod (Cod p)
+
+class (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category (Dom2 p), Category (Cod2 p)) => Bifunctor (p :: i -> j -> k)
+instance  (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category (Dom2 p), Category (Cod2 p)) => Bifunctor (p :: i -> j -> k)
+
+first :: (Functor f, Cod f ~ Nat d e, Ob d c) => Dom f a b -> e (f a c) (f b c)
+first = runNat . fmap
+
+second :: forall p a b c. (Bifunctor p, Ob (Dom p) c) => Dom2 p a b -> Cod2 p (p c a) (p c b)
+second f = case ob :: Ob (Dom p) c :- FunctorOf (Dom2 p) (Cod2 p) (p c) of
+  Sub Dict -> fmap f
 
+bimap :: Bifunctor p => Dom p a b -> Dom2 p c d -> Cod2 p (p a c) (p b d)
+bimap f g = case source f of
+  Dict -> case target g of
+    Dict -> runNat (fmap f) . second g
 
+-- mapping over a profunctor 
+dimap :: Bifunctor p => Op (Dom p) b a -> Dom2 p c d -> Cod2 p (p a c) (p b d)
+dimap = bimap . unop

src/Math/Groupoid.hs

@@ -1,7 +1,12 @@
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
 module Math.Groupoid where
 
 import Math.Category
 
 class Category p => Groupoid p where
   inv :: p a b -> p b a
+
+instance (Groupoid p, Op p ~ Yoneda p) => Groupoid (Yoneda p) where
+  inv (Op f) = Op (inv f)

src/Math/Multicategory.hs

@@ -1,41 +1,63 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE GADTs #-}
-module Math.Multicategory where
+
+module Math.Multicategory 
+  ( Forest(..)
+  , Multicategory(..)
+  -- * Utilities 
+  , inputs, outputs
+  , splitForest
+  ) where
 
 import Data.Constraint
+import Data.Proxy
 import Math.Category
 import Math.Rec
 import Math.Rec.All
+import Prelude (($), undefined)
 
 data Forest :: ([i] -> i -> *) -> [i] -> [i] -> * where
   Nil :: Forest f '[] '[]
-  Cons :: f k o -> Forest f m n -> Forest f (k ++ m) (o ': n)
+  (:-) :: f k o -> Forest f m n -> Forest f (k ++ m) (o ': n)
 
 inputs  :: forall f g is os. (forall as b. f as b -> Rec g as) -> Forest f is os -> Rec g is
 inputs _ Nil = RNil 
-inputs f (Cons a as) = f a `appendRec` inputs f as
+inputs f (a :- as) = f a `appendRec` inputs f as
 
 outputs :: (forall as b. f as b -> p b) -> Forest f is os -> Rec p os
 outputs f Nil = RNil
-outputs f (Cons a as) = f a :& outputs f as
+outputs f (a :- as) = f a :& outputs f as
+
+splitForest :: forall f g ds is js os r. Rec f is -> Forest g js os -> Forest g ds (is ++ js) -> (forall bs cs. (ds ~ (bs ++ cs)) => Forest g bs is -> Forest g cs js -> r) -> r
+splitForest RNil bs as k = k Nil as
+splitForest (i :& is) bs ((j :: g as o) :- js) k = splitForest is bs js $ \ (l :: Forest g bs as1) (r :: Forest g cs js) ->
+  case appendAssocAxiom (Proxy :: Proxy as) (Proxy :: Proxy bs) (Proxy :: Proxy cs) of
+    Dict -> k (j :- l) r
 
 class Multicategory (f :: [i] -> i -> *) where
   type Mob f :: i -> Constraint
   type Mob f = Vacuous
-  ident    :: Mob f a => f '[a] a
-  compose  :: f bs c -> Forest f as bs -> f as c
-  msources :: f as b -> Rec (Dict1 (Mob f)) as
-  mtarget  :: f as b -> Dict (Mob f b)
+  ident   :: Mob f a => f '[a] a
+  compose :: f bs c -> Forest f as bs -> f as c
+  sources :: f as b -> Rec (Dict1 (Mob f)) as
+  mtarget :: f as b -> Dict1 (Mob f) b
 
 instance Multicategory f => Category (Forest f) where
   type Ob (Forest f) = All (Mob f)
-  id = undefined -- Cons ident Nil
-  (.) = undefined
-  source = undefined
-  target = undefined
+  id = go proofs where
+    go :: Rec (Dict1 (Mob f)) is -> Forest f is is
+    go (Dict1 :& as) = ident :- idents as
+    go RNil          = Nil
+
+  Nil . Nil = Nil
+  (b :- bs) . as = splitForest (sources b) bs as $ \es fs -> compose b es :- (bs . fs)
+
+  source = reproof . inputs sources
+  target = reproof . outputs mtarget

src/Math/Rec/All.hs

@@ -29,6 +29,7 @@ instance All p '[] where
 instance (p i, All p is) => All p (i ': is) where
   proofs = Dict1 :& proofs
 
+-- TODO: unsafeCoerce 
 reproof :: Rec (Dict1 p) is -> Dict (All p is)
 reproof RNil = Dict
 reproof (Dict1 :& as) = case reproof as of