Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions Announcement.md
Original file line number Diff line number Diff line change
Expand Up @@ -128,11 +128,11 @@ endofunctor typeclasses, which may be used to provide a familiar
API for the free category functor.

```Haskell
class QFunctor c where
qmap :: (forall x y. p x y -> q x y) -> c p x y -> c q x y
class QFunctor c => QPointed c where
qsingle :: p x y -> c p x y
class QFunctor c => QFoldable c where
class BifunctorFunctor c where
bifmap :: (forall x y. p x y -> q x y) -> c p x y -> c q x y
class BifunctorFunctor c => QPointed c where
bireturn :: p x y -> c p x y
class BifunctorFunctor c => QFoldable c where
qfoldMap :: Category q => (forall x y. p x y -> q x y) -> c p x y -> q x y
```

Expand All @@ -152,7 +152,7 @@ such that

and that these functions characterize `c` up to isomorphism as a universal property.

But, `u` and `i` have the same type signatures as `qfoldMap` and `qsingle`.
But, `u` and `i` have the same type signatures as `qfoldMap` and `bireturn`.
So, you can characterize the free category abstractly as a constraint.

```Haskell
Expand Down
2 changes: 2 additions & 0 deletions free-categories.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -20,5 +20,7 @@ library
Data.Quiver.Bifunctor
Data.Quiver.Functor
build-depends: base >=4.12 && <=5
, bifunctors
, profunctors
hs-source-dirs: src
default-language: Haskell2010
46 changes: 25 additions & 21 deletions src/Control/Category/Free.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@ of the category of quivers with,
* @t (g . f) = t g . t f@

Thus, a functor from quivers to `Category`s
has @(QFunctor c, forall p. Category (c p))@ with.
has @(BifunctorFunctor c, forall p. Category (c p))@ with.

prop> qmap f id = id
prop> qmap f (q . p) = qmap f q . qmap f p
prop> bifmap f id = id
prop> bifmap f (q . p) = bifmap f q . bifmap f p

The [free category functor](https://ncatlab.org/nlab/show/free+category)
from quivers to `Category`s may be defined up to isomorphism as
Expand All @@ -42,24 +42,26 @@ from quivers to `Category`s may be defined up to isomorphism as
, QuantifiedConstraints
, RankNTypes
, StandaloneDeriving
, TypeOperators
#-}

module Control.Category.Free
( Path (..)
, pattern (:<<)
, FoldPath (..)
, CFree (..)
, CFree
, toPath
, reversePath
, beforeAll
, afterAll
, Category (..)
) where

import Data.Bifunctor.Functor
import Data.Profunctor.Cayley
import Data.Quiver
import Data.Quiver.Functor
import Control.Category
import Control.Monad (join)
import Prelude hiding (id, (.))

{- | A `Path` with steps in @p@ is a singly linked list of
Expand Down Expand Up @@ -90,9 +92,9 @@ instance Category (Path p) where
(.) path = \case
Done -> path
p :>> ps -> p :>> (ps >>> path)
instance QFunctor Path where
qmap _ Done = Done
qmap f (p :>> ps) = f p :>> qmap f ps
instance BifunctorFunctor Path where
bifmap _ Done = Done
bifmap f (p :>> ps) = f p :>> bifmap f ps
instance QFoldable Path where
qfoldMap _ Done = id
qfoldMap f (p :>> ps) = f p >>> qfoldMap f ps
Expand All @@ -105,8 +107,9 @@ instance QFoldable Path where
instance QTraversable Path where
qtraverse _ Done = pure Done
qtraverse f (p :>> ps) = (:>>) <$> f p <*> qtraverse f ps
instance QPointed Path where qsingle p = p :>> Done
instance QMonad Path where qjoin = qfold
instance BifunctorMonad Path where
bireturn p = p :>> Done
bijoin = qfold
instance CFree Path

{- | Encodes a path as its `qfoldMap` function.-}
Expand All @@ -118,12 +121,13 @@ instance x ~ y => Monoid (FoldPath p x y) where mempty = id
instance Category (FoldPath p) where
id = FoldPath $ \ _ -> id
FoldPath g . FoldPath f = FoldPath $ \ k -> g k . f k
instance QFunctor FoldPath where qmap f = qfoldMap (qsingle . f)
instance BifunctorFunctor FoldPath where bifmap f = qfoldMap (bireturn . f)
instance QFoldable FoldPath where qfoldMap k (FoldPath f) = f k
instance QTraversable FoldPath where
qtraverse f = getApQ . qfoldMap (ApQ . fmap qsingle . f)
instance QPointed FoldPath where qsingle p = FoldPath $ \ k -> k p
instance QMonad FoldPath where qjoin (FoldPath f) = f id
qtraverse f = runCayley . qfoldMap (Cayley . fmap bireturn . f)
instance BifunctorMonad FoldPath where
bireturn p = FoldPath $ \ k -> k p
bijoin (FoldPath f) = f id
instance CFree FoldPath

{- | Unpacking the definition of a left adjoint to the forgetful functor
Expand All @@ -133,11 +137,11 @@ from `Category`s to quivers, any

factors uniquely through the free `Category` @c@ as

prop> qfoldMap f . qsingle = f
prop> qfoldMap f . bireturn = f
-}
class
( QPointed c
, QFoldable c
( BifunctorMonad c
, QTraversable c
, forall p. Category (c p)
) => CFree c where

Expand All @@ -146,20 +150,20 @@ It is the unique isomorphism which exists
between any two `CFree` functors.
-}
toPath :: (QFoldable c, CFree path) => c p x y -> path p x y
toPath = qfoldMap qsingle
toPath = qfoldMap bireturn

{- | Reverse all the arrows in a path. -}
reversePath :: (QFoldable c, CFree path) => c p x y -> path (OpQ p) y x
reversePath = getOpQ . qfoldMap (OpQ . qsingle . OpQ)
reversePath = getOpQ . qfoldMap (OpQ . bireturn . OpQ)

{- | Insert a given loop before each step. -}
beforeAll
:: (QFoldable c, CFree path)
=> (forall x. p x x) -> c p x y -> path p x y
beforeAll sep = qfoldMap (\p -> qsingle sep >>> qsingle p)
beforeAll sep = qfoldMap (\p -> bireturn sep >>> bireturn p)

{- | Insert a given loop before each step. -}
afterAll
:: (QFoldable c, CFree path)
=> (forall x. p x x) -> c p x y -> path p x y
afterAll sep = qfoldMap (\p -> qsingle p >>> qsingle sep)
afterAll sep = qfoldMap (\p -> bireturn p >>> bireturn sep)
73 changes: 3 additions & 70 deletions src/Data/Quiver.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,25 +26,20 @@ Many Haskell typeclasses are constraints on quivers, such as
, QuantifiedConstraints
, RankNTypes
, StandaloneDeriving
, TypeOperators
#-}

module Data.Quiver
( IQ (..)
, OpQ (..)
, IsoQ (..)
, ApQ (..)
, KQ (..)
, ProductQ (..)
, qswap
, HomQ (..)
, ReflQ (..)
, ComposeQ (..)
, LeftQ (..)
, RightQ (..)
) where

import Control.Category
import Control.Monad (join)
import Data.Bifunctor.Functor
import Prelude hiding (id, (.))

{- | The identity functor on quivers. -}
Expand Down Expand Up @@ -74,16 +69,6 @@ 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]
Expand All @@ -97,29 +82,11 @@ 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 }
instance BifunctorFunctor (HomQ p) where bifmap g (HomQ f) = HomQ (g . f)

{- | A term in @ReflQ r x y@ observes the equality @x ~ y@.

Expand All @@ -133,37 +100,3 @@ 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)
Loading