{-|
Module: Data.Quiver
Description: free categories
Copyright: (c) Eitan Chatav, 2019
Maintainer: eitan@morphism.tech
Stability: experimental
A [quiver](https://ncatlab.org/nlab/show/quiver)
is a directed graph where loops and multiple arrows
between vertices are allowed, a multidigraph. A Haskell quiver
is a higher kinded type,
@p :: k -> k -> Type@
* where vertices are types @x :: k@,
* and arrows from @x@ to @y@ are terms @p :: p x y@.
Many Haskell typeclasses are constraints on quivers, such as
`Category`, `Data.Bifunctor.Bifunctor`,
@Profunctor@, and `Control.Arrow.Arrow`.
-}
{-# LANGUAGE
GADTs
, PolyKinds
, QuantifiedConstraints
, RankNTypes
, StandaloneDeriving
#-}
module Data.Quiver
( IQ (..)
, OpQ (..)
, IsoQ (..)
, ApQ (..)
, KQ (..)
, ProductQ (..)
, qswap
, HomQ (..)
, ReflQ (..)
, ComposeQ (..)
, LeftQ (..)
, RightQ (..)
) where
import Control.Category
import Control.Monad (join)
import Prelude hiding (id, (.))
{- | The identity functor on quivers. -}
newtype IQ c x y = IQ {getIQ :: c x y} deriving (Eq, Ord, Show)
instance (Category c, x ~ y) => Semigroup (IQ c x y) where (<>) = (>>>)
instance (Category c, x ~ y) => Monoid (IQ c x y) where mempty = id
instance Category c => Category (IQ c) where
id = IQ id
IQ g . IQ f = IQ (g . f)
{- | Reverse all the arrows in a quiver.-}
newtype OpQ c x y = OpQ {getOpQ :: c y x} deriving (Eq, Ord, Show)
instance (Category c, x ~ y) => Semigroup (OpQ c x y) where (<>) = (>>>)
instance (Category c, x ~ y) => Monoid (OpQ c x y) where mempty = id
instance Category c => Category (OpQ c) where
id = OpQ id
OpQ g . OpQ f = OpQ (f . g)
{- | Arrows of `IsoQ` are bidirectional edges.-}
data IsoQ c x y = IsoQ
{ up :: c x y
, down :: c y x
} deriving (Eq, Ord, Show)
instance (Category c, x ~ y) => Semigroup (IsoQ c x y) where (<>) = (>>>)
instance (Category c, x ~ y) => Monoid (IsoQ c x y) where mempty = id
instance Category c => Category (IsoQ c) where
id = IsoQ id id
(IsoQ yz zy) . (IsoQ xy yx) = IsoQ (yz . xy) (yx . zy)
{- | Apply a constructor to the arrows of a quiver.-}
newtype ApQ m c x y = ApQ {getApQ :: m (c x y)} deriving (Eq, Ord, Show)
instance (Applicative m, Category c, x ~ y)
=> Semigroup (ApQ m c x y) where (<>) = (>>>)
instance (Applicative m, Category c, x ~ y)
=> Monoid (ApQ m c x y) where mempty = id
instance (Applicative m, Category c) => Category (ApQ m c) where
id = ApQ (pure id)
ApQ g . ApQ f = ApQ ((.) <$> g <*> f)
{- | The constant quiver.
@KQ ()@ is an [indiscrete category]
(https://ncatlab.org/nlab/show/indiscrete+category).
-}
newtype KQ r x y = KQ {getKQ :: r} deriving (Eq, Ord, Show)
instance (Semigroup m, x ~ y) => Semigroup (KQ m x y) where
KQ f <> KQ g = KQ (f <> g)
instance (Monoid m, x ~ y) => Monoid (KQ m x y) where mempty = id
instance Monoid m => Category (KQ m) where
id = KQ mempty
KQ g . KQ f = KQ (f <> g)
{- | [Cartesian monoidal product]
(https://ncatlab.org/nlab/show/cartesian+monoidal+category)
of quivers.-}
data ProductQ p q x y = ProductQ
{ qfst :: p x y
, qsnd :: q x y
} deriving (Eq, Ord, Show)
instance (Category p, Category q, x ~ y)
=> Semigroup (ProductQ p q x y) where (<>) = (>>>)
instance (Category p, Category q, x ~ y)
=> Monoid (ProductQ p q x y) where mempty = id
instance (Category p, Category q) => Category (ProductQ p q) where
id = ProductQ id id
ProductQ pyz qyz . ProductQ pxy qxy = ProductQ (pyz . pxy) (qyz . qxy)
{- | Symmetry of `ProductQ`.-}
qswap :: ProductQ p q x y -> ProductQ q p x y
qswap (ProductQ p q) = ProductQ q p
{- | The quiver of quiver morphisms, `HomQ` is the [internal hom]
(https://ncatlab.org/nlab/show/internal+hom)
of the category of quivers.-}
newtype HomQ p q x y = HomQ { getHomQ :: p x y -> q x y }
{- | A term in @ReflQ r x y@ observes the equality @x ~ y@.
@ReflQ ()@ is the [discrete category]
(https://ncatlab.org/nlab/show/discrete+category).
-}
data ReflQ r x y where ReflQ :: r -> ReflQ r x x
deriving instance Show r => Show (ReflQ r x y)
deriving instance Eq r => Eq (ReflQ r x y)
deriving instance Ord r => Ord (ReflQ r x y)
instance Monoid m => Category (ReflQ m) where
id = ReflQ mempty
ReflQ yz . ReflQ xy = ReflQ (xy <> yz)
{- | Compose quivers along matching source and target.-}
data ComposeQ p q x z = forall y. ComposeQ (p y z) (q x y)
deriving instance (forall y. Show (p y z), forall y. Show (q x y))
=> Show (ComposeQ p q x z)
instance (Category p, p ~ q, x ~ y)
=> Semigroup (ComposeQ p q x y) where (<>) = (>>>)
instance (Category p, p ~ q, x ~ y)
=> Monoid (ComposeQ p q x y) where mempty = id
instance (Category p, p ~ q) => Category (ComposeQ p q) where
id = ComposeQ id id
ComposeQ yz xy . ComposeQ wx vw = ComposeQ (yz . xy) (wx . vw)
{- | The left [residual]
(https://ncatlab.org/nlab/show/residual)
of `ComposeQ`.-}
newtype LeftQ p q x y = LeftQ
{getLeftQ :: forall w. p w x -> q w y}
instance (p ~ q, x ~ y) => Semigroup (LeftQ p q x y) where (<>) = (>>>)
instance (p ~ q, x ~ y) => Monoid (LeftQ p q x y) where mempty = id
instance p ~ q => Category (LeftQ p q) where
id = LeftQ id
LeftQ g . LeftQ f = LeftQ (g . f)
{- | The right [residual]
(https://ncatlab.org/nlab/show/residual)
of `ComposeQ`.-}
newtype RightQ p q x y = RightQ
{getRightQ :: forall z. p y z -> q x z}
instance (p ~ q, x ~ y) => Semigroup (RightQ p q x y) where (<>) = (>>>)
instance (p ~ q, x ~ y) => Monoid (RightQ p q x y) where mempty = id
instance p ~ q => Category (RightQ p q) where
id = RightQ id
RightQ f . RightQ g = RightQ (g . f)