proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Instance.Free

Description

The category freely generated by a quiver p of generator arrows, extended with a chosen list cs of structural classes (terminal object, products, closed structure, ...): an arrow of FREE cs p is a formal composite of generators (Emb) and structure morphisms (St). fold interprets such an arrow in any category supporting the same structures, making this the basis for deeply embedded categorical DSLs.

For a quiver with no structures, Proarrow.Category.Instance.Paths fits better: its objects are the vertices themselves, which keep the base kind's Ob and can be taken apart.

No equations: only the category laws hold structurally (composition is a normalized spine). For example fst . (f &&& g) and f are different Free values. Two arrows are equal when every fold identifies them, so decide equality by interpreting into a concrete category, not by pattern matching.

An object is a shape (IsFreeOb), asking nothing of k beyond being a category. Its denotation along a functor f out of k is Lower f a, and withLowerOb recovers that denotation's Ob in fold.

Classes imposing type equalities (like Cartesian's tensor = product) cannot be listed in cs, since each carrier is fixed (** is always the formal tensor). A kind wrapper can recover the instance: PROD (FREE '[HasTerminalObject, HasBinaryProducts] p) is a free cartesian category.

Synopsis

Documentation

type family All (cs :: [Kind -> Constraint]) k where ... Source Github #

Equations

All ('[] :: [Kind -> Constraint]) k = () 
All (c ': cs) k = (c k, All cs k) 

class Elem (c :: Kind -> Constraint) (cs :: [Kind -> Constraint]) where Source Github #

Membership of a structure in the list, with the entailment All cs k => c k as a method rather than a quantified superclass: as a given, the quantified form would shadow the ordinary instances for the free category itself and demand All cs (FREE cs p).

Methods

fromAll :: All cs k => (c k => r) -> r Source Github #

Instances

Instances details
Elem c (c ': cs) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

fromAll :: All (c ': cs) k => (c k => r) -> r Source Github #

Elem c cs => Elem c (d ': cs) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

fromAll :: All (d ': cs) k => (c k => r) -> r Source Github #

type family Elems (ds :: [Kind -> Constraint]) (cs :: [Kind -> Constraint]) where ... Source Github #

Membership of several structures at once: '[Monoidal, SymMonoidal] `Elems` cs.

Equations

Elems ('[] :: [Kind -> Constraint]) cs = () 
Elems (d ': ds) cs = (Elem d cs, Elems ds cs) 

data FREE (cs :: [Kind -> Constraint]) (p :: CAT k) Source Github #

The objects of the free category over the quiver p on k: the embedded objects of k (EMB) plus one object former per structure in cs (products, exponentials, ...), which live in their structures' modules.

Constructors

EMB k 

Instances

Instances details
Elem Monoidal cs => IsFreeOb (UnitF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (UnitF :: FREE cs p)) => r) -> r Source Github #

Elem HasInitialObject cs => IsFreeOb (InitF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (InitF :: FREE cs p)) => r) -> r Source Github #

Elem HasTerminalObject cs => IsFreeOb (TermF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (TermF :: FREE cs p)) => r) -> r Source Github #

(IsFreeOb a, Elem StarAutonomous cs) => IsFreeOb (DualF a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (DualF a)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elem Monoidal cs) => IsFreeOb (a **! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a **! b)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elems ClosedStructures cs) => IsFreeOb (a --> b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a --> b)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elem HasBinaryCoproducts cs) => IsFreeOb (a + b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a + b)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elem HasBinaryProducts cs) => IsFreeOb (a *! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a *! b)) => r) -> r Source Github #

KnownCtx ('[] :: [Syntax k]) Source Github # 
Instance details

Defined in Proarrow.Tools.CCC

Methods

ctxOb :: Obj (Mul ('[] :: [Syntax k])) Source Github #

Elem HasBinaryCoproducts cs => Site Sums (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Sheaf

Methods

legArrow :: forall (a :: FREE cs p) c (x :: FREE cs p). Leg Sums (FREE cs p) a c x -> x ~> a Source Github #

legs :: forall (a :: FREE cs p) c. Cover Sums (FREE cs p) a c -> [SomeLeg Sums (FREE cs p) a c] Source Github #

(KnownCtx i, Ob b) => KnownCtx (b ': i :: [Syntax k]) Source Github # 
Instance details

Defined in Proarrow.Tools.CCC

Methods

ctxOb :: Obj (Mul (b ': i)) Source Github #

(Elem HasBinaryCoproducts cs, Elem HasInitialObject cs, CategoryOf j) => Sheaf Sums (Yo x ('OP b) :: FREE cs p -> j -> Type) Source Github #

Sums are colimits, so the representables are sheaves for Sums: gluing is ||| on the contravariant component.

The initial object is needed too. An element of Yo x (OP b) also has a covariant component b ~> d. A family over the two injections has one per leg, and the glued element only one. Matching forces the two to agree because the injections overlap at the initial object, lft . initiate = rgt . initiate. Without it every family matches vacuously, and restriction fails for any j with a hom-set bigger than one.

Instance details

Defined in Proarrow.Category.Sheaf

Methods

glue :: forall (a :: FREE cs p) c (b0 :: j). (Ob a, Ob b0) => Cover Sums (FREE cs p) a c -> (forall (x0 :: FREE cs p). Leg Sums (FREE cs p) a c x0 -> Yo x ('OP b) x0 b0) -> Yo x ('OP b) a b0 Source Github #

Discrete k => FunctorForRep (Embed :: k +-> FREE ds p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

fmap :: forall (a :: k) (b :: k). (a ~> b) -> ((Embed :: k +-> FREE ds p) @ a) ~> ((Embed :: k +-> FREE ds p) @ b) Source Github #

Elem Monoidal cs => Monoidal (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Monoidal

type Unit = UnitF :: FREE cs p

Methods

withOb2 :: forall (a :: FREE cs p) (b :: FREE cs p) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: FREE cs p). Ob a => ((Unit :: FREE cs p) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: FREE cs p). Ob a => a ~> ((Unit :: FREE cs p) ** a) Source Github #

rightUnitor :: forall (a :: FREE cs p). Ob a => (a ** (Unit :: FREE cs p)) ~> a Source Github #

rightUnitorInv :: forall (a :: FREE cs p). Ob a => a ~> (a ** (Unit :: FREE cs p)) Source Github #

associator :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

Elems SymMonoidalStructures cs => SymMonoidal (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

swap :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Elems ClosedStructures cs => Closed (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

withObExp :: forall (a :: FREE cs p) (b :: FREE cs p) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: FREE cs p) (b :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

Elems CompactClosedStructures cs => CompactClosed (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.CompactClosed

Methods

distribDual :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => Dual (a ** b) ~> (Dual a ** Dual b) Source Github #

dualUnit :: Dual (Unit :: FREE cs p) ~> (Unit :: FREE cs p) Source Github #

dualityUnit :: forall (a :: FREE cs p). Ob a => (Unit :: FREE cs p) ~> (a ** Dual a) Source Github #

dualityCounit :: forall (a :: FREE cs p). Ob a => (Dual a ** a) ~> (Unit :: FREE cs p) Source Github #

Elems DistributiveStructures cs => Distributive (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Distributive

Methods

distL :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: FREE cs p). Ob a => (a ** (InitialObject :: FREE cs p)) ~> (InitialObject :: FREE cs p) Source Github #

absorbR :: forall (a :: FREE cs p). Ob a => ((InitialObject :: FREE cs p) ** a) ~> (InitialObject :: FREE cs p) Source Github #

(Supplies Frobenius (FREE cs p), CompactClosed (FREE cs p)) => Hypergraph (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Hypergraph

Elems StarAutonomousStructures cs => StarAutonomous (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Methods

withObDual :: forall (a :: FREE cs p) r. Ob a => (Ob (Dual a) => r) -> r Source Github #

dual :: forall (a :: FREE cs p) (b :: FREE cs p). (a ~> b) -> Dual b ~> Dual a Source Github #

dualInv :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Github #

linDist :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

doubleNeg :: forall (a :: FREE cs p). Ob a => Dual (Dual a) ~> a Source Github #

doubleNegInv :: forall (a :: FREE cs p). Ob a => a ~> Dual (Dual a) Source Github #

Elem HasBinaryCoproducts cs => HasBinaryCoproducts (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

withObCoprod :: forall (a :: FREE cs p) (b :: FREE cs p) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: FREE cs p) (a :: FREE cs p) (y :: FREE cs p). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: FREE cs p) (b :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

Elem HasInitialObject cs => HasInitialObject (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject 
Instance details

Defined in Proarrow.Colimit.Initial

type InitialObject = InitF :: FREE cs p

Methods

initiate :: forall (a :: FREE cs p). Ob a => (InitialObject :: FREE cs p) ~> a Source Github #

CategoryOf (FREE cs p) Source Github #

The category freely generated from the heteromorphisms of p, together with formal structure arrows for each of the classes in cs. An object is a shape (IsFreeOb).

Instance details

Defined in Proarrow.Category.Instance.Free

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.Free

type (~>) = Free :: FREE cs p -> FREE cs p -> Type
Elem HasBinaryProducts cs => HasBinaryProducts (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

withObProd :: forall (a :: FREE cs p) (b :: FREE cs p) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: FREE cs p) (b :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

Elem HasTerminalObject cs => HasTerminalObject (FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject 
Instance details

Defined in Proarrow.Limit.Terminal

type TerminalObject = TermF :: FREE cs p

Methods

terminate :: forall (a :: FREE cs p). Ob a => a ~> (TerminalObject :: FREE cs p) Source Github #

(CommutativeMonoid a, CocommutativeComonoid a) => Frobenius (a :: FREE cs p) Source Github #

In the free category the supply generators (see Supplies Monoid/Supplies Comonoid in Proarrow.Monoid) are compatible by fiat, so monoid + comonoid is already Frobenius. With both supplies in cs, Supplies Frobenius and Hypergraph are derived, with no structure of their own. Superclasses are taken directly as the context to keep dictionary construction acyclic. Bundling them into an All-style constraint here builds a dictionary that references itself through the quantified Supplies constraint, looping at runtime.

Instance details

Defined in Proarrow.Category.Monoidal.Hypergraph

(Comonoid a, SymMonoidal (FREE cs p)) => CocommutativeComonoid (a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Monoid

(Monoid a, SymMonoidal (FREE cs p)) => CommutativeMonoid (a :: FREE cs p) Source Github #

The free supply is commutative only up to interpretation (FREE has no equations); the marker holds because every fold of these arrows into a target lands in that target's commutative monoid.

Instance details

Defined in Proarrow.Monoid

(Elems '[Supplies Comonoid, Monoidal] cs, Ob a) => Comonoid (a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Monoid

Methods

counit :: a ~> (Unit :: FREE cs p) Source Github #

comult :: a ~> (a ** a) Source Github #

(Elems '[Supplies Monoid, Monoidal] cs, Ob a) => Monoid (a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Monoid

Methods

mempty :: (Unit :: FREE cs p) ~> a Source Github #

mappend :: (a ** a) ~> a Source Github #

Promonad (Free :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

id :: forall (a :: FREE cs p). Ob a => Free a a Source Github #

(.) :: forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p). Free b c -> Free a b -> Free a c Source Github #

Elem Monoidal cs => MonoidalProfunctor (Free :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

one :: Free (Unit :: FREE cs p) (Unit :: FREE cs p) Source Github #

(**) :: forall (x1 :: FREE cs p) (x2 :: FREE cs p) (y1 :: FREE cs p) (y2 :: FREE cs p). Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2) Source Github #

Profunctor (Free :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

dimap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p) (d :: FREE cs p). (c ~> a) -> (b ~> d) -> Free a b -> Free c d Source Github #

lmap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p). (c ~> a) -> Free a b -> Free c b Source Github #

rmap :: forall (b :: FREE cs p) (d :: FREE cs p) (a :: FREE cs p). (b ~> d) -> Free a b -> Free a d Source Github #

(\\) :: forall (a :: FREE cs p) (b :: FREE cs p) r. ((Ob a, Ob b) => r) -> Free a b -> r Source Github #

type Lower (f :: k +-> k') (UnitF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

type Lower (f :: k +-> k') (UnitF :: FREE cs p) = Unit :: k'
type Lower (f :: k +-> k') (InitF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

type Lower (f :: k +-> k') (InitF :: FREE cs p) = InitialObject :: k'
type Lower (f :: k +-> k') (TermF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

type Lower (f :: k +-> k') (TermF :: FREE cs p) = TerminalObject :: k'
type Lower (f :: k1 +-> k2) (DualF a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

type Lower (f :: k1 +-> k2) (DualF a :: FREE cs p) = Dual (Lower f a)
type Lower (f :: k +-> k') (a **! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

type Lower (f :: k +-> k') (a **! b :: FREE cs p) = Lower f a ** Lower f b
type Lower (f :: k +-> k') (a --> b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type Lower (f :: k +-> k') (a --> b :: FREE cs p) = Lower f a ~~> Lower f b
type Lower (f :: k +-> k') (a + b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type Lower (f :: k +-> k') (a + b :: FREE cs p) = Lower f a || Lower f b
type Lower (f :: k +-> k') (a *! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Lower (f :: k +-> k') (a *! b :: FREE cs p) = Lower f a && Lower f b
data Cover Sums (FREE cs p) (a :: FREE cs p) c Source Github # 
Instance details

Defined in Proarrow.Category.Sheaf

data Cover Sums (FREE cs p) (a :: FREE cs p) c where
data Leg Sums (FREE cs p) (a :: FREE cs p) c (z :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Sheaf

data Leg Sums (FREE cs p) (a :: FREE cs p) c (z :: FREE cs p) where
type (Embed :: k +-> FREE ds p) @ (a :: k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

type (Embed :: k +-> FREE ds p) @ (a :: k) = 'EMB a :: FREE ds p
type Unit Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

type Unit = UnitF :: FREE cs p
type InitialObject Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

type InitialObject = InitF :: FREE cs p
type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

type (~>) = Free :: FREE cs p -> FREE cs p -> Type
type TerminalObject Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

type TerminalObject = TermF :: FREE cs p
type Dual (a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

type Dual (a :: FREE cs p) = DualF a
type Ob (a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

type Ob (a :: FREE cs p) = IsFreeOb a
type (a :: FREE cs p) ** (b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

type (a :: FREE cs p) ** (b :: FREE cs p) = a **! b
type (a :: FREE cs p) ~~> (b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type (a :: FREE cs p) ~~> (b :: FREE cs p) = a --> b
type (a :: FREE cs p) || (b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type (a :: FREE cs p) || (b :: FREE cs p) = a + b
type (a :: FREE cs p) && (b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: FREE cs p) && (b :: FREE cs p) = a *! b

data Free (a :: FREE cs p) (b :: FREE cs p) where Source Github #

Arrows of the free category: a right-associated composition spine ending in Nil, with a generator (Emb) or structure morphism (St) precomposed onto the rest at each step, so the category laws hold definitionally. The fields are linear (%1) so that DSL helpers built on Free can offer HOAS-style binders whose bound variable must be used exactly once.

Constructors

Nil :: forall {k} {cs :: [Kind -> Constraint]} {p :: CAT k} (a :: FREE cs p). Ob a => Free a a 
Emb :: forall {k} (a1 :: k) (b1 :: k) (p :: CAT k) (cs :: [Kind -> Constraint]) (a :: FREE cs p). (Ob a1, Ob b1) => p a1 b1 -> Free a ('EMB a1 :: FREE cs p) -> Free a ('EMB b1 :: FREE cs p) 
St :: forall {k} {cs :: [Kind -> Constraint]} {p :: CAT k} (c :: Kind -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p) (a :: FREE cs p). (HasStructure cs p c, Ob a1, Ob b) => Struct c a1 b -> Free a a1 -> Free a b 

Instances

Instances details
Promonad (Free :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

id :: forall (a :: FREE cs p). Ob a => Free a a Source Github #

(.) :: forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p). Free b c -> Free a b -> Free a c Source Github #

Elem Monoidal cs => MonoidalProfunctor (Free :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

one :: Free (Unit :: FREE cs p) (Unit :: FREE cs p) Source Github #

(**) :: forall (x1 :: FREE cs p) (x2 :: FREE cs p) (y1 :: FREE cs p) (y2 :: FREE cs p). Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2) Source Github #

Profunctor (Free :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

dimap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p) (d :: FREE cs p). (c ~> a) -> (b ~> d) -> Free a b -> Free c d Source Github #

lmap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p). (c ~> a) -> Free a b -> Free c b Source Github #

rmap :: forall (b :: FREE cs p) (d :: FREE cs p) (a :: FREE cs p). (b ~> d) -> Free a b -> Free a d Source Github #

(\\) :: forall (a :: FREE cs p) (b :: FREE cs p) r. ((Ob a, Ob b) => r) -> Free a b -> r Source Github #

WithShow a => Show (Free a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

showsPrec :: Int -> Free a b -> ShowS Github #

show :: Free a b -> String Github #

showList :: [Free a b] -> ShowS Github #

emb :: forall {k} (a :: k) (b :: k) p (cs :: [Kind -> Constraint]). (Ob a, Ob b) => p a b %1 -> Free ('EMB a :: FREE cs p) ('EMB b :: FREE cs p) Source Github #

class Show2 p => WithShow (a :: FREE c p) Source Github #

Instances

Instances details
Show2 p => WithShow (a :: FREE c p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

showPostComp :: forall {k} {cs :: [Kind -> Constraint]} {p1 :: CAT k} p2 (a :: FREE cs p1) (b :: FREE cs p1). (Show p2, WithShow a) => Int -> p2 -> Free a b -> ShowS Source Github #

class IsFreeOb (a :: FREE cs p) where Source Github #

The shape of an object of the free category, by object former. This is Ob for the free category. It carries the shape's denotation Lower along any functor out of k, and how to recover that denotation's Ob from the leaves' (lowerOb, normally used through withLowerOb and withLowerIdOb).

Associated Types

type Lower (f :: k +-> k') (a :: FREE cs p) :: k' Source Github #

The denotation of the object along a functor f out of k. (The class variable is re-annotated here so that k is in scope before f's kind mentions it.)

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f a) => r) -> r Source Github #

Instances

Instances details
Elem Monoidal cs => IsFreeOb (UnitF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (UnitF :: FREE cs p)) => r) -> r Source Github #

Elem HasInitialObject cs => IsFreeOb (InitF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (InitF :: FREE cs p)) => r) -> r Source Github #

Elem HasTerminalObject cs => IsFreeOb (TermF :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (TermF :: FREE cs p)) => r) -> r Source Github #

(IsFreeOb a, Elem StarAutonomous cs) => IsFreeOb (DualF a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (DualF a)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elem Monoidal cs) => IsFreeOb (a **! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a **! b)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elems ClosedStructures cs) => IsFreeOb (a --> b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a --> b)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elem HasBinaryCoproducts cs) => IsFreeOb (a + b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a + b)) => r) -> r Source Github #

(IsFreeOb a, IsFreeOb b, Elem HasBinaryProducts cs) => IsFreeOb (a *! b :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a *! b)) => r) -> r Source Github #

Ob a => IsFreeOb ('EMB a :: FREE cs p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f ('EMB a :: FREE cs p)) => r) -> r Source Github #

withLowerOb :: forall {k} {k'} {cs :: [Kind -> Constraint]} {p :: CAT k} (f :: k +-> k') (a :: FREE cs p) r. (IsFreeOb a, Representable f, All cs k') => (Ob (Lower f a) => r) -> r Source Github #

Ob (Lower f a) from the shape of a, for interpreting along f.

withLowerIdOb :: forall {k} {cs :: [Kind -> Constraint]} {p :: CAT k} (a :: FREE cs p) r. (IsFreeOb a, CategoryOf k, All cs k) => (Ob (Lower (Id :: k -> k -> Type) a) => r) -> r Source Github #

withLowerOb along the identity: the Ob of a shape's denotation in k itself, when k happens to carry the structures cs.

class (Show2 p => Show2 str) => CanShow (str :: CAT (FREE cs p)) Source Github #

Instances

Instances details
(Show2 p => Show2 str) => CanShow (str :: FREE cs p -> FREE cs p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

class (CanShow (Struct c :: CAT (FREE cs p)), Elem c cs) => HasStructure (cs :: [Kind -> Constraint]) (p :: CAT k) (c :: Kind -> Constraint) where Source Github #

Associated Types

data Struct (c :: Kind -> Constraint) :: CAT (FREE cs p) Source Github #

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (c k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct c a b -> Lower f a ~> Lower f b Source Github #

Instances

Instances details
Elem Monoidal cs => HasStructure cs (p :: CAT k) Monoidal Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Associated Types

data Struct Monoidal (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal

data Struct Monoidal (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (Monoidal k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct Monoidal a b -> Lower f a ~> Lower f b Source Github #

Elems SymMonoidalStructures cs => HasStructure cs (p :: CAT k) SymMonoidal Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Associated Types

data Struct SymMonoidal (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal

data Struct SymMonoidal (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (SymMonoidal k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct SymMonoidal a b -> Lower f a ~> Lower f b Source Github #

Elems '[Cartesian, HasTerminalObject, HasBinaryProducts, Monoidal] cs => HasStructure cs (p :: CAT k) Cartesian Source Github #

The free-category structure for Cartesian. The free category cannot satisfy the /type equality/ tensor = product (TensorIsProduct fails on it, see Proarrow.Category.Instance.Free), but it can carry the corresponding isomorphisms as formal arrows, interpreted to the identity in any cartesian target (productToTensor and friends). So a free category can serve as syntax for cartesian (closed) categories without collapsing its object grammar.

Instance details

Defined in Proarrow.Category.Monoidal.Cartesian

Associated Types

data Struct Cartesian (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal.Cartesian

data Struct Cartesian (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (Cartesian k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct Cartesian a b -> Lower f a ~> Lower f b Source Github #

Elems ClosedStructures cs => HasStructure cs (p :: CAT k) Closed Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

Associated Types

data Struct Closed (a :: FREE cs p) (b :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

data Struct Closed (a :: FREE cs p) (b :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (Closed k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct Closed a b -> Lower f a ~> Lower f b Source Github #

Elems CompactClosedStructures cs => HasStructure cs (p :: CAT k) CompactClosed Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.CompactClosed

Associated Types

data Struct CompactClosed (a :: FREE cs p) (b :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal.CompactClosed

data Struct CompactClosed (a :: FREE cs p) (b :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (CompactClosed k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct CompactClosed a b -> Lower f a ~> Lower f b Source Github #

Elems DistributiveStructures cs => HasStructure cs (p :: CAT k) Distributive Source Github #

The free-category structure for Distributive: formal distributors and absorbers, interpreted by foldStructure through the target's own. Together with the coproduct and monoidal structures this makes a free category over a bare quiver distributive without asking anything of the quiver's category.

Instance details

Defined in Proarrow.Category.Monoidal.Distributive

Associated Types

data Struct Distributive (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal.Distributive

data Struct Distributive (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (Distributive k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct Distributive a b -> Lower f a ~> Lower f b Source Github #

Elems StarAutonomousStructures cs => HasStructure cs (p :: CAT k) StarAutonomous Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Associated Types

data Struct StarAutonomous (a :: FREE cs p) (b :: FREE cs p) 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

data Struct StarAutonomous (a :: FREE cs p) (b :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (StarAutonomous k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct StarAutonomous a b -> Lower f a ~> Lower f b Source Github #

Elem HasBinaryCoproducts cs => HasStructure cs (p :: CAT k) HasBinaryCoproducts Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Associated Types

data Struct HasBinaryCoproducts (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

data Struct HasBinaryCoproducts (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (HasBinaryCoproducts k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct HasBinaryCoproducts a b -> Lower f a ~> Lower f b Source Github #

Elem HasInitialObject cs => HasStructure cs (p :: CAT k) HasInitialObject Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

data Struct HasInitialObject (a :: FREE cs p) (b :: FREE cs p) 
Instance details

Defined in Proarrow.Colimit.Initial

data Struct HasInitialObject (a :: FREE cs p) (b :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (HasInitialObject k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct HasInitialObject a b -> Lower f a ~> Lower f b Source Github #

Elem HasBinaryProducts cs => HasStructure cs (p :: CAT k) HasBinaryProducts Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

data Struct HasBinaryProducts (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

data Struct HasBinaryProducts (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (HasBinaryProducts k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct HasBinaryProducts a b -> Lower f a ~> Lower f b Source Github #

Elem HasTerminalObject cs => HasStructure cs (p :: CAT k) HasTerminalObject Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

data Struct HasTerminalObject (a :: FREE cs p) (b :: FREE cs p) 
Instance details

Defined in Proarrow.Limit.Terminal

data Struct HasTerminalObject (a :: FREE cs p) (b :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (HasTerminalObject k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct HasTerminalObject a b -> Lower f a ~> Lower f b Source Github #

Elems '[Supplies Comonoid, Monoidal] cs => HasStructure cs (p :: CAT k) (Supplies Comonoid) Source Github #

The free-category structure for Supplies Comonoid, dually: formal comult (Fork) and counit (Prune) generators for every object.

Instance details

Defined in Proarrow.Monoid

Associated Types

data Struct (Supplies Comonoid) (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Monoid

data Struct (Supplies Comonoid) (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (Supplies Comonoid k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct (Supplies Comonoid) a b -> Lower f a ~> Lower f b Source Github #

Elems '[Supplies Monoid, Monoidal] cs => HasStructure cs (p :: CAT k) (Supplies Monoid) Source Github #

The free-category structure for Supplies Monoid: every object gets formal mappend (Join) and mempty (Sprout) generators, interpreted by foldStructure through the target's own supply.

Instance details

Defined in Proarrow.Monoid

Associated Types

data Struct (Supplies Monoid) (i :: FREE cs p) (o :: FREE cs p) 
Instance details

Defined in Proarrow.Monoid

data Struct (Supplies Monoid) (i :: FREE cs p) (o :: FREE cs p) where

Methods

foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (Supplies Monoid k', All cs k', Representable f) => (forall (x :: FREE cs p) (y :: FREE cs p). (x ~> y) -> Lower f x ~> Lower f y) -> Struct (Supplies Monoid) a b -> Lower f a ~> Lower f b Source Github #

fold :: forall {k} {k'} {p} (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p). (All cs k', Representable f) => (forall (x :: k) (y :: k). (Ob x, Ob y) => p x y -> (f % x) ~> (f % y)) -> (a ~> b) -> Lower f a ~> Lower f b Source Github #

Interpret a free arrow along a functor f into any category k' supporting the structures cs, given an interpretation of the generators between the images of their objects. This is the universal property of the free category. The interpreter is handed (Ob x, Ob y) explicitly (the evidence bundled on Emb), because a bare quiver p is not a Profunctor, so the Obs cannot be recovered from the value.

retract :: forall {k} {k'} (cs :: [Kind -> Constraint]) (f :: k +-> k') (a :: FREE cs (InitialProfunctor :: k -> k -> Type)) (b :: FREE cs (InitialProfunctor :: k -> k -> Type)). (All cs k', Representable f) => (a ~> b) -> Lower f a ~> Lower f b Source Github #

liftFree :: forall {k} (cs :: [Kind -> Constraint]) (x :: k) (y :: k). CategoryOf k => (x ~> y) -> ('EMB x :: FREE cs ((~>) :: CAT k)) ~> ('EMB y :: FREE cs ((~>) :: CAT k)) Source Github #

Taking the quiver to be the hom of a category k makes FREE cs (Hom k) the free cs-structured category over k: liftFree embeds the arrows of k as generators, and when k itself already has the structures, retractFree interprets back into k along the identity. These back the free-kind instances of HasFreeK (e.g. the free category with a terminal object, or with binary products, over k).

retractFree :: forall (cs :: [Kind -> Constraint]) {k} (a :: FREE cs (Hom k)) (b :: FREE cs ((~>) :: CAT k)). (CategoryOf k, All cs k) => (a ~> b) -> Lower (Id :: k -> k -> Type) a ~> Lower (Id :: k -> k -> Type) b Source Github #

data family Embed :: k +-> FREE ds p Source Github #

The object-embedding functor a |-> EMB a of a widening (see widen), as a representable profunctor. The base kind must be Discrete, since arrows of k other than identities have no counterpart in the free category.

Instances

Instances details
Discrete k => FunctorForRep (Embed :: k +-> FREE ds p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

Methods

fmap :: forall (a :: k) (b :: k). (a ~> b) -> ((Embed :: k +-> FREE ds p) @ a) ~> ((Embed :: k +-> FREE ds p) @ b) Source Github #

type (Embed :: k +-> FREE ds p) @ (a :: k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Free

type (Embed :: k +-> FREE ds p) @ (a :: k) = 'EMB a :: FREE ds p

widen :: forall (ds :: [Kind -> Constraint]) {k} {cs :: [Kind -> Constraint]} {p :: CAT k} (a :: FREE cs p) (b :: FREE cs p). (All cs (FREE ds p), Discrete k) => (a ~> b) -> Lower (Rep (Embed :: k +-> FREE ds p)) a ~> Lower (Rep (Embed :: k +-> FREE ds p)) b Source Github #

Widen a free arrow into a free category over a larger structure list: fold along Embed, so each structural object is rebuilt as itself in the larger category (e.g. the terminal object lowers to the target's terminal object) and generators embed as generators. The All cs (FREE ds p) constraint is the evidence that every structure in cs is also available in ds.