Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Paths

Description

The category freely generated by a quiver p: an arrow is a finite path of generators (PCons onto PNil), and an object is simply a vertex.

This is Proarrow.Category.Instance.Free without structures. With no formal products or exponentials to form, the objects can be the vertices themselves, with Ob inherited from the base kind, so an object of PATHS p can be taken apart by whatever that Ob provides. An object of the free structured category cannot, since Lower/lowerOb never yields a value indexed by a shape. An empty structure list does not help: the pattern checker cannot rule out the HasStructure given of St, so every consumer would carry an unreachable branch.

Equations are supported, by Rewrite. Composition only adds an arrow at the outer end of the spine, so each new arrow can be normalised against an already-normal path. With the default rewrite the category is free.

The base kind must be a category because foldPaths interprets along a functor out of it, and functors are representable profunctors here. Its arrows are never used, so the intended base is a discrete one.

Synopsis

data PATHS (p :: CAT k) = PTH k
data Paths (a :: PATHS p) (b :: PATHS p) where
- PNil :: forall {k} {p :: CAT k} (a1 :: k). Ob a1 => Paths ('PTH a1 :: PATHS p) ('PTH a1 :: PATHS p)
- PCons :: forall {k} (a1 :: k) (b1 :: k) (p :: CAT k) (a :: PATHS p). (Ob a1, Ob b1) => p a1 b1 -> Paths a ('PTH a1 :: PATHS p) -> Paths a ('PTH b1 :: PATHS p)
class Rewrite (p :: CAT k) where
- rewrite :: forall (a :: k) (b :: k) (i :: PATHS p). (Ob a, Ob b) => p a b -> Paths i ('PTH a :: PATHS p) -> Paths i ('PTH b :: PATHS p)
class EqGen (p :: CAT k) where
- eqGen :: forall (x :: k) (b :: k) (y :: k). p x b -> p y b -> Maybe (x :~: y)
pathLength :: forall {k} {p :: CAT k} (a :: PATHS p) (b :: PATHS p). Paths a b -> Int
emb :: forall {k} (a :: k) (b :: k) p. (Ob a, Ob b, Rewrite p) => p a b -> ('PTH a :: PATHS p) ~> ('PTH b :: PATHS p)
foldPaths :: forall {k} {k'} {p} (f :: PATHS p +-> k') (a :: k) (b :: k). Representable f => (forall (x :: k) r. Ob x => (Ob (f % ('PTH x :: PATHS p)) => r) -> r) -> (forall (x :: k) (y :: k). (Ob x, Ob y) => p x y -> (f % ('PTH x :: PATHS p)) ~> (f % ('PTH y :: PATHS p))) -> (('PTH a :: PATHS p) ~> ('PTH b :: PATHS p)) -> (f % ('PTH a :: PATHS p)) ~> (f % ('PTH b :: PATHS p))

Documentation

data PATHS (p :: CAT k) Source Github #

The objects of the free category on p: its vertices.

Constructors

PTH k

Instances

Instances details

(Enumerable k, Rewrite p) => Enumerable (PATHS p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

Methods

withIndex :: forall (a :: PATHS p) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: PATHS p) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (PATHS p) (At (PATHS p) i) Source Github #

Finite k => Finite (PATHS p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

Associated Types

type Objects (PATHS p)
Instance details Defined in Proarrow.Category.Instance.Paths type Objects (PATHS p) = MapWrap ('PTH :: k -> PATHS p) (Objects k)

Methods

finite :: IndexedList (Objects (PATHS p)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (PATHS p)) i ~ At (PATHS p) i => r) -> r Source Github #

Indexed k => Indexed (PATHS p) Source Github #

Objects are vertices, so a free category has as many of them as its quiver has, however many arrows the paths add (usually unboundedly many). So a free category is Finite without being anywhere near thin or decidable. This buys enumeration of the objects alone. That is enough for Proarrow.Testing.genSomeFinite to derive a schema's object palette, and not enough for anything that wants to enumerate arrows.

Instance details

Defined in Proarrow.Category.Instance.Paths

(CategoryOf k, Rewrite p) => CategoryOf (PATHS p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Paths type (~>) = Paths :: PATHS p -> PATHS p -> Type

(CategoryOf k, Rewrite p) => Promonad (Paths :: PATHS p -> PATHS p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

Methods

id :: forall (a :: PATHS p). Ob a => Paths a a Source Github #

(.) :: forall (b :: PATHS p) (c :: PATHS p) (a :: PATHS p). Paths b c -> Paths a b -> Paths a c Source Github #

(CategoryOf k, Rewrite p) => Profunctor (Paths :: PATHS p -> PATHS p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

Methods

dimap :: forall (c :: PATHS p) (a :: PATHS p) (b :: PATHS p) (d :: PATHS p). (c ~> a) -> (b ~> d) -> Paths a b -> Paths c d Source Github #

lmap :: forall (c :: PATHS p) (a :: PATHS p) (b :: PATHS p). (c ~> a) -> Paths a b -> Paths c b Source Github #

rmap :: forall (b :: PATHS p) (d :: PATHS p) (a :: PATHS p). (b ~> d) -> Paths a b -> Paths a d Source Github #

(\\) :: forall (a :: PATHS p) (b :: PATHS p) r. ((Ob a, Ob b) => r) -> Paths a b -> r Source Github #

type Objects (PATHS p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

type Objects (PATHS p) = MapWrap ('PTH :: k -> PATHS p) (Objects k)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

type (~>) = Paths :: PATHS p -> PATHS p -> Type

type At (PATHS p) i Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

type At (PATHS p) i = FmapWrap ('PTH :: k -> PATHS p) (At k i)

type Index (a :: PATHS p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

type Index (a :: PATHS p) = Index (UN ('PTH :: k -> PATHS p) a)

type Ob (a :: PATHS p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Paths

type Ob (a :: PATHS p) = WrappedOb ('PTH :: k -> PATHS p) a

data Paths (a :: PATHS p) (b :: PATHS p) where Source Github #

A path of generators, as a right-associated spine, so that the category laws hold definitionally.

Constructors

PNil :: forall {k} {p :: CAT k} (a1 :: k). Ob a1 => Paths ('PTH a1 :: PATHS p) ('PTH a1 :: PATHS p)
PCons :: forall {k} (a1 :: k) (b1 :: k) (p :: CAT k) (a :: PATHS p). (Ob a1, Ob b1) => p a1 b1 -> Paths a ('PTH a1 :: PATHS p) -> Paths a ('PTH b1 :: PATHS p)

Instances

Instances details

(CategoryOf k, Rewrite p) => Promonad (Paths :: PATHS p -> PATHS p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Paths Methods id :: forall (a :: PATHS p). Ob a => Paths a a Source Github # (.) :: forall (b :: PATHS p) (c :: PATHS p) (a :: PATHS p). Paths b c -> Paths a b -> Paths a c Source Github #
(CategoryOf k, Rewrite p) => Profunctor (Paths :: PATHS p -> PATHS p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Paths Methods dimap :: forall (c :: PATHS p) (a :: PATHS p) (b :: PATHS p) (d :: PATHS p). (c ~> a) -> (b ~> d) -> Paths a b -> Paths c d Source Github # lmap :: forall (c :: PATHS p) (a :: PATHS p) (b :: PATHS p). (c ~> a) -> Paths a b -> Paths c b Source Github # rmap :: forall (b :: PATHS p) (d :: PATHS p) (a :: PATHS p). (b ~> d) -> Paths a b -> Paths a d Source Github # (\\) :: forall (a :: PATHS p) (b :: PATHS p) r. ((Ob a, Ob b) => r) -> Paths a b -> r Source Github #
Show2 p => Show (Paths a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.Paths Methods showsPrec :: Int -> Paths a b -> ShowS Github # show :: Paths a b -> String Github # showList :: [Paths a b] -> ShowS Github #
EqGen p => Eq (Paths a b) Source Github #	Structural equality of paths. This is equality of arrows exactly when `rewrite` is confluent and every path was built through `emb`, `id` and composition, which keep paths in normal form. The free structured category cannot offer this: there, equality has to be decided by folding both sides into some category that identifies them.
Instance details Defined in Proarrow.Category.Instance.Paths Methods (==) :: Paths a b -> Paths a b -> Bool Github # (/=) :: Paths a b -> Paths a b -> Bool Github #

class Rewrite (p :: CAT k) where Source Github #

The equations of the generated category, as a rewriting system on paths. rewrite is handed a generator and the already-normalised path it is being composed onto, and returns the normal form of the two together; the default keeps the path as it is, which generates the free category.

An equation is one clause. For Secr ⨟ WorksIn = id, match the junction and drop both arrows:

rewrite WorksIn (PCons Secr more) = more

The whole tail is in scope, so a longer left-hand side can be matched, and recursing on the result renormalises a junction the rewrite has just exposed.

Confluence and termination are the caller's to establish. Nothing here checks them, and a system that lacks them breaks associativity of composition silently. Two further obligations come with any non-default instance: foldPaths is a functor only for interpretations that respect the equations, and so is any other consumer that matches on generators.

Minimal complete definition

Nothing

Methods

rewrite :: forall (a :: k) (b :: k) (i :: PATHS p). (Ob a, Ob b) => p a b -> Paths i ('PTH a :: PATHS p) -> Paths i ('PTH b :: PATHS p) Source Github #

class EqGen (p :: CAT k) where Source Github #

Decidable equality of generators, which also has to decide their sources: the object between two arrows of a path is existential, so Eq (p x y) alone cannot compare two spines. (Eq2 does not serve. It is equality of arrows of a fixed category, as isMono wants.)

Methods

eqGen :: forall (x :: k) (b :: k) (y :: k). p x b -> p y b -> Maybe (x :~: y) Source Github #

pathLength :: forall {k} {p :: CAT k} (a :: PATHS p) (b :: PATHS p). Paths a b -> Int Source Github #

How many generators a path is made of. With a non-default rewrite this is a way to see that an equation fired, since a path that reduces comes out shorter.

emb :: forall {k} (a :: k) (b :: k) p. (Ob a, Ob b, Rewrite p) => p a b -> ('PTH a :: PATHS p) ~> ('PTH b :: PATHS p) Source Github #

A single generator, normalised. Named as in Proarrow.Category.Instance.Free.

foldPaths :: forall {k} {k'} {p} (f :: PATHS p +-> k') (a :: k) (b :: k). Representable f => (forall (x :: k) r. Ob x => (Ob (f % ('PTH x :: PATHS p)) => r) -> r) -> (forall (x :: k) (y :: k). (Ob x, Ob y) => p x y -> (f % ('PTH x :: PATHS p)) ~> (f % ('PTH y :: PATHS p))) -> (('PTH a :: PATHS p) ~> ('PTH b :: PATHS p)) -> (f % ('PTH a :: PATHS p)) ~> (f % ('PTH b :: PATHS p)) Source Github #

Interpret a path in any category, given an interpretation of the generators: the universal property of the free category. A functor out of PATHS p is a map of vertices plus such an interpretation, with nothing to check, since a quiver has no composition to preserve.

The first argument supplies Ob of an image object. It cannot come from f by withObRep: the usual caller is f's own fmap, which would loop on the empty path. For unconstrained objects pass \r -> r.