module Hask.Rep where
import Hask.Core
import Hask.Prof
class Representable (p :: x -> y -> z) where
type Rep p :: y -> x
_Rep :: Iso (p a b) (p a' b') (Hom a (Rep p b)) (Hom a' (Rep p b'))
instance Representable (->) where
type Rep (->) = Id
_Rep = un (mapping _Id)
instance Representable (Nat :: (i -> *) -> (i -> *) -> *) where
type Rep (Nat :: (i -> *) -> (i -> *) -> *) = Id
_Rep = un (mapping _Id)
instance Representable (:-) where
type Rep (:-) = Id
_Rep = un (mapping _Id)
instance Representable (Down f) where
type Rep (Down f) = f
_Rep = dimap runDown Down
instance ( Representable p
, Representable q
, Composed (Hom :: i -> i -> *)
, Functor (Rep q)
, Category (Hom :: i -> i -> *)
, Category (Hom :: j -> j -> *)
) => Representable (Prof (p :: j -> k -> *) (q :: i -> j -> *)) where
type Rep (Prof p q) = Rep q · Rep p
_Rep = dimap (\(Prof p q) -> compose . fmap (get _Rep p) . get _Rep q)
(\k -> Prof (beget _Rep id) (beget _Rep (decompose . k)))
class Corepresentable (p :: x -> y -> z) where
type Corep p :: x -> y
_Corep :: Iso (p a b) (p a' b') (Hom (Corep p a) b) (Hom (Corep p a') b')
instance Corepresentable (->) where
type Corep (->) = Id
_Corep = lmapping _Id
instance Corepresentable (Nat :: (i -> *) -> (i -> *) -> *) where
type Corep (Nat :: (i -> *) -> (i -> *) -> *) = Id
_Corep = lmapping _Id
instance Corepresentable (:-) where
type Corep (:-) = Id
_Corep = lmapping _Id
instance Corepresentable (Up f) where
type Corep (Up f) = f
_Corep = dimap runUp Up
instance ( Corepresentable p
, Corepresentable q
, Composed (Hom :: k -> k -> *)
, Functor (Corep p)
, Category (Hom :: j -> j -> *)
, Category (Hom :: k -> k -> *)
) => Corepresentable (Prof (p :: j -> k -> *) (q :: i -> j -> *)) where
type Corep (Prof p q) = Corep p · Corep q
_Corep = dimap (\(Prof p q) -> get _Corep p . fmap (get _Corep q) . decompose)
(\k -> Prof (beget _Corep (k . compose)) (beget _Corep id))
instance Corepresentable (|-) where
type Corep (|-) = IdC
_Corep = lmapping _Id
data Up f a b = Up { runUp :: f a ~> b }
_Up = dimap runUp Up
instance Category (Hom :: j -> j -> *) => Contravariant (Up :: (i -> j) -> i -> j -> *) where
contramap f = nat2 $ _Up (. runNat f)
instance (Functor f, Category (Cod f)) => Contravariant (Up f) where
contramap f = Nat $ _Up (. fmap f)
instance Category (Cod f) => Functor (Up f a) where
fmap f = _Up (f .)
instance Precartesian (Cod f) => Semimonoidal (Up f a) where
ap2 (f, g) = Up $ runUp f &&& runUp g
instance (Precartesian (Cod f), Semigroup b) => Semigroup (Up f a b) where
mult = multM
instance (Cartesian (Cod f), Monoid b) => Monoid (Up f a b) where
one = oneM
instance Cartesian (Cod f) => Monoidal (Up f a) where
ap0 () = Up terminal
instance Semimonad (Up f a) where
join k = Up $ \a -> runUp (runUp k a) a
data Down f a b = Down { runDown :: a ~> f b }
_Down = dimap runDown Down
instance Category (Hom :: i -> i -> *) => Functor (Down :: (j -> i) -> i -> j -> *) where
fmap f = nat2 $ _Down (runNat f .)
instance Category (Cod f) => Contravariant (Down f) where
contramap f = Nat $ _Down (. f)
instance (Functor f, Category (Cod f)) => Functor (Down f a) where
fmap f = _Down (fmap f .)
instance Semimonoidal f => Semimonoidal (Down f a) where
ap2 (f, g) = Down $ ap2 . (runDown f &&& runDown g)
instance Monoidal f => Monoidal (Down f a) where
ap0 () = Down $ ap0 . terminal
instance Semimonad f => Semimonad (Down f a) where
join f = Down $ \r -> join $ fmap (\g -> runDown g r) $ runDown f r
instance (Semimonoidal f, Semigroup b) => Semigroup (Down f a b) where
mult = multM
instance (Monoidal f, Monoid b) => Monoid (Down f a b) where
one = oneM