module Hask.Category
(
Category'(..)
, Category''
, Category
, Functor(..)
, FunctorOf
, ob, obOf
, contramap
, Bifunctor
, Cod2, Dom2
, fmap1, first
, bimap
, dimap
, Vacuous
, Constraint, (:-)(Sub), Dict(..), (\\), sub, Class(cls), (:=>)(ins)
, Yoneda(..), Op, Opd
, Nat(..), NatId, Endo, nat, (!)
, Presheaves, Copresheaves
, NatDom, NatCod
, ($), Either(..)
, Fix(..)
) where
import Data.Constraint (Constraint, (:-)(Sub), Dict(..), (\\), Class(cls), (:=>)(ins))
import qualified Data.Constraint as Constraint
import Data.Proxy (Proxy(..))
import Prelude (($), Either(..))
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 Category' (p :: i -> i -> *) where
type Ob p :: i -> Constraint
id :: Ob p a => p a a
observe :: p a b -> Dict (Ob p a, Ob p b)
(.) :: p b c -> p a b -> p a c
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
type Endo p a = p a a
class (Category' (Dom f), Category' (Cod 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)
class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
ob :: forall f a. Functor f => Ob (Dom f) a :- Ob (Cod f) (f a)
ob = Sub $ case observe (fmap (id :: Dom f a a) :: Cod f (f a) (f a)) of
Dict -> Dict
data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where
Nat :: ( FunctorOf p q f
, FunctorOf p q g
) => {
runNat :: forall a. Ob p a => q (f a) (g a)
} -> Nat p q f g
type NatId p = Endo (Nat (Dom p) (Cod p)) p
obOf :: (Category (Dom f), Category (Cod f)) => NatId f -> Endo (Dom f) a
-> Dict (Ob (Nat (Dom f) (Cod f)) f, Ob (Dom f) a, Ob (Cod f) (f a))
obOf f a = case observe f of
Dict -> case observe a of
Dict -> case observe (f ! a) of
Dict -> Dict
type Copresheaves p = Nat p (->)
type Presheaves p = Nat (Op p) (->)
instance (Category' p, Category' q) => Functor (FunctorOf p q) where
type Dom (FunctorOf p q) = Nat p q
type Cod (FunctorOf p q) = (:-)
fmap Nat{} = Sub Dict
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)
fmap1 :: forall p a b c. (Bifunctor p, Ob (Dom p) c) => Dom2 p a b -> Cod2 p (p c a) (p c b)
fmap1 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 observe f of
Dict -> case observe g of
Dict -> runNat (fmap f) . fmap1 g
type Opd f = Op (Dom f)
contramap :: Functor f => Opd f b a -> Cod f (f a) (f b)
contramap = fmap . unop
dimap :: Bifunctor p => Opd p b a -> Dom2 p c d -> Cod2 p (p a c) (p b d)
dimap = bimap . unop
class (Category' p, Bifunctor p, Dom p ~ Op p, p ~ Op (Dom p), Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->)) => Category'' p
instance (Category' p, Bifunctor p, Dom p ~ Op p, p ~ Op (Dom p), Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->)) => Category'' p
class (Category'' p, Category'' (Op p), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category p
instance (Category'' p, Category'' (Op p), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category p
class Vacuous (c :: i -> i -> *) (a :: i)
instance Vacuous c a
instance Functor Dict where
type Dom Dict = (:-)
type Cod Dict = (->)
fmap f Dict = case f of Sub g -> g
instance (Category' c, Ob c ~ Vacuous c) => Functor (Vacuous c) where
type Dom (Vacuous c) = c
type Cod (Vacuous c) = (:-)
fmap _ = Sub Dict
instance Functor (:-) where
type Dom (:-) = Op (:-)
type Cod (:-) = Nat (:-) (->)
fmap (Op f) = Nat (. f)
instance Functor ((:-) b) where
type Dom ((:-) a) = (:-)
type Cod ((:-) a) = (->)
fmap = (.)
instance Category' (:-) where
type Ob (:-) = Vacuous (:-)
id = Constraint.refl
observe _ = Dict
(.) = Constraint.trans
unop = getOp
sub :: (a => Proxy a -> Dict b) -> a :- b
sub k = Sub (k Proxy)
instance Functor (->) where
type Dom (->) = Op (->)
type Cod (->) = Nat (->) (->)
fmap (Op f) = Nat (. f)
instance Functor ((->)a) where
type Dom ((->) a) = (->)
type Cod ((->) a) = (->)
fmap = (.)
instance Category' (->) where
type Ob (->) = Vacuous (->)
id x = x
observe _ = Dict
(.) f g x = f (g x)
unop = getOp
instance (Category p, Op p ~ Yoneda p) => Functor (Yoneda p) where
type Dom (Yoneda p) = p
type Cod (Yoneda p) = Nat (Yoneda p) (->)
fmap f = Nat (. Op f)
instance (Category p, Op p ~ Yoneda p) => Functor (Yoneda p a) where
type Dom (Yoneda p a) = Yoneda p
type Cod (Yoneda p a) = (->)
fmap = (.)
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)
observe (Op f) = case observe f of
Dict -> Dict
unop = Op
op = getOp
instance (Category' p, Category q) => Functor (Nat p q) where
type Dom (Nat p q) = Op (Nat p q)
type Cod (Nat p q) = Nat (Nat p q) (->)
fmap (Op f) = Nat (. f)
instance (Category' p, Category q) => Functor (Nat p q a) where
type Dom (Nat p q f) = Nat p q
type Cod (Nat p q f) = (->)
fmap = (.)
instance (Category' p, Category' q) => Category' (Nat p q) where
type Ob (Nat p q) = FunctorOf p q
id = Nat id1 where
id1 :: forall f x. (Functor f, Dom f ~ p, Cod f ~ q, Ob p x) => q (f x) (f x)
id1 = id \\ (ob :: Ob p x :- Ob q (f x))
observe Nat{} = Dict
Nat f . Nat g = Nat (f . g)
unop = getOp
nat :: (Category p ,Category q, FunctorOf p q f, FunctorOf p q g) => (forall a. Ob p a => Endo p a -> q (f a) (g a)) -> Nat p q f g
nat k = Nat (k id)
infixr 1 !
(!) :: Nat p q f g -> p a a -> q (f a) (g a)
Nat n ! f = case observe f of
Dict -> n
instance Functor (,) where
type Dom (,) = (->)
type Cod (,) = Nat (->) (->)
fmap f = Nat $ \(a,b) -> (f a, b)
instance Functor ((,) a) where
type Dom ((,) a) = (->)
type Cod ((,) a) = (->)
fmap f (a,b) = (a, f 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
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)
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
newtype Fix (f :: * -> * -> *) (a :: *) = In { out :: f (Fix f a) a }
instance Functor Fix where
type Dom Fix = Nat (->) (Nat (->) (->))
type Cod Fix = Nat (->) (->)
fmap f = case observe f of
Dict -> Nat $ \ (In mu) -> In (first (first f) (runNat (runNat f) mu))
instance FunctorOf (->) (Nat (->) (->)) p => Functor (Fix p) where
type Dom (Fix f) = (->)
type Cod (Fix f) = (->)
fmap f (In b) = In (bimap (fmap f) f b)