Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.FreeBiCCC

Description

The free bicartesian closed category on a generating profunctor p.

Unlike Proarrow.Category.Instance.Free (which is generic over an arbitrary list of structures), this is hardcoded to exactly the BiCCC signature, to simplify the implementation.

Synopsis

data FBC (p :: k +-> k)
- = OBJ k
- | UNIT
- | PROD (FBC p) (FBC p)
- | ZERO
- | SUM (FBC p) (FBC p)
- | EXPO (FBC p) (FBC p)
data Term (a :: FBC p) (b :: FBC p) where
- Id :: forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
- Compose :: forall {k} {p :: k +-> k} (b1 :: FBC p) (b :: FBC p) (a :: FBC p). Term b1 b -> Term a b1 -> Term a b
- Emb :: forall {k} (x :: k) (y :: k) (p :: k +-> k). (Ob x, Ob y) => p x y -> Term ('OBJ x :: FBC p) ('OBJ y :: FBC p)
- Terminate :: forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a ('UNIT :: FBC p)
- Absurd :: forall {k} {p :: k +-> k} (b :: FBC p). Ob b => Term ('ZERO :: FBC p) b
- Fst :: forall {k} {p :: k +-> k} (b :: FBC p) (b1 :: FBC p). (Ob b, Ob b1) => Term ('PROD b b1) b
- Snd :: forall {k} {p :: k +-> k} (a1 :: FBC p) (b :: FBC p). (Ob a1, Ob b) => Term ('PROD a1 b) b
- Pair :: forall {k} {p :: k +-> k} (a :: FBC p) (a1 :: FBC p) (b1 :: FBC p). Term a a1 -> Term a b1 -> Term a ('PROD a1 b1)
- Inl :: forall {k} {p :: k +-> k} (a :: FBC p) (b1 :: FBC p). (Ob a, Ob b1) => Term a ('SUM a b1)
- Inr :: forall {k} {p :: k +-> k} (a1 :: FBC p) (a :: FBC p). (Ob a1, Ob a) => Term a ('SUM a1 a)
- Case :: forall {k} {p :: k +-> k} (a1 :: FBC p) (b :: FBC p) (b1 :: FBC p). Term a1 b -> Term b1 b -> Term ('SUM a1 b1) b
- Curry :: forall {k} {p :: k +-> k} (a :: FBC p) (b1 :: FBC p) (c :: FBC p). (Ob a, Ob b1) => Term ('PROD a b1) c -> Term a ('EXPO b1 c)
- Apply :: forall {k} {p :: k +-> k} (a1 :: FBC p) (b :: FBC p). (Ob a1, Ob b) => Term ('PROD ('EXPO a1 b) a1) b
type family Lower (a :: FBC p) :: k where ...
interp :: forall {k} p (src :: FBC p) (tgt :: FBC p). BiCCC k => (forall (x :: k) (y :: k). p x y -> x ~> y) -> Term src tgt -> Lower src ~> Lower tgt
class KnownFBCOb (a :: FBC p) where
- fbcCase :: (forall (x :: k). (a ~ ('OBJ x :: FBC p), Ob x) => r) -> (a ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (a ~ 'PROD x y, Ob x, Ob y) => r) -> (a ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (a ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). (a ~ 'EXPO x y, Ob x, Ob y) => r) -> r
fbcOb :: forall {k} {p :: k +-> k} (a :: FBC p). (BiCCC k, KnownFBCOb a) => Term a a

Documentation

data FBC (p :: k +-> k) Source Github #

Object expressions of the free BiCCC on generators p: base objects (OBJ, carrying an actual object of k — the category p's generating morphisms are themselves between), plus terminal/initial objects and products, coproducts and exponentials of sub-expressions.

Constructors

OBJ k
UNIT
PROD (FBC p) (FBC p)
ZERO
SUM (FBC p) (FBC p)
EXPO (FBC p) (FBC p)

Instances

Instances details

BiCCC k => Monoidal (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC type Unit = TerminalObject :: FBC p

Methods

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

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

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

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

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

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

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

BiCCC k => SymMonoidal (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

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

BiCCC k => Closed (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

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

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

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

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

BiCCC k => HasBinaryCoproducts (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

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

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

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

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

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

BiCCC k => HasInitialObject (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC type InitialObject = 'ZERO :: FBC p

Methods

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

BiCCC k => CategoryOf (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC type (~>) = Term :: FBC p -> FBC p -> Type

BiCCC k => HasBinaryProducts (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

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

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

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

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

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

BiCCC k => HasTerminalObject (FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC type TerminalObject = 'UNIT :: FBC p

Methods

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

BiCCC k => Promonad (Term :: FBC p -> FBC p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

id :: forall (a :: FBC p). Ob a => Term a a Source Github #

(.) :: forall (b :: FBC p) (c :: FBC p) (a :: FBC p). Term b c -> Term a b -> Term a c Source Github #

BiCCC k => MonoidalProfunctor (Term :: FBC p -> FBC p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

one :: Term (Unit :: FBC p) (Unit :: FBC p) Source Github #

(**) :: forall (x1 :: FBC p) (x2 :: FBC p) (y1 :: FBC p) (y2 :: FBC p). Term x1 x2 -> Term y1 y2 -> Term (x1 ** y1) (x2 ** y2) Source Github #

BiCCC k => Profunctor (Term :: FBC p -> FBC p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

Methods

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

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

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

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

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type Unit = TerminalObject :: FBC p

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type InitialObject = 'ZERO :: FBC p

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type (~>) = Term :: FBC p -> FBC p -> Type

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type TerminalObject = 'UNIT :: FBC p

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

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type Ob (a :: FBC p) = (Ob (Lower a), KnownFBCOb a)

type (a :: FBC p) ** (b :: FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type (a :: FBC p) ** (b :: FBC p) = a && b

type (a :: FBC p) ~~> (b :: FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type (a :: FBC p) ~~> (b :: FBC p) = 'EXPO a b

type (a :: FBC p) || (b :: FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type (a :: FBC p) || (b :: FBC p) = 'SUM a b

type (a :: FBC p) && (b :: FBC p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FreeBiCCC

type (a :: FBC p) && (b :: FBC p) = 'PROD a b

data Term (a :: FBC p) (b :: FBC p) where Source Github #

A term of the free BiCCC: one constructor per operation, including composition itself. No smart constructors, no normal forms — e.g. Compose Id f and f are different Terms that happen to interpret to the same morphism. p (and the base category k it's a profunctor on) is carried purely by the kind of a/b (FBC p), the same way Proarrow.Category.Instance.Free's Free carries its generating profunctor, so it doesn't need to be an explicit parameter of Term itself.

Constructors

Id :: forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Compose :: forall {k} {p :: k +-> k} (b1 :: FBC p) (b :: FBC p) (a :: FBC p). Term b1 b -> Term a b1 -> Term a b
Emb :: forall {k} (x :: k) (y :: k) (p :: k +-> k). (Ob x, Ob y) => p x y -> Term ('OBJ x :: FBC p) ('OBJ y :: FBC p)
Terminate :: forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a ('UNIT :: FBC p)
Absurd :: forall {k} {p :: k +-> k} (b :: FBC p). Ob b => Term ('ZERO :: FBC p) b
Fst :: forall {k} {p :: k +-> k} (b :: FBC p) (b1 :: FBC p). (Ob b, Ob b1) => Term ('PROD b b1) b
Snd :: forall {k} {p :: k +-> k} (a1 :: FBC p) (b :: FBC p). (Ob a1, Ob b) => Term ('PROD a1 b) b
Pair :: forall {k} {p :: k +-> k} (a :: FBC p) (a1 :: FBC p) (b1 :: FBC p). Term a a1 -> Term a b1 -> Term a ('PROD a1 b1)
Inl :: forall {k} {p :: k +-> k} (a :: FBC p) (b1 :: FBC p). (Ob a, Ob b1) => Term a ('SUM a b1)
Inr :: forall {k} {p :: k +-> k} (a1 :: FBC p) (a :: FBC p). (Ob a1, Ob a) => Term a ('SUM a1 a)
Case :: forall {k} {p :: k +-> k} (a1 :: FBC p) (b :: FBC p) (b1 :: FBC p). Term a1 b -> Term b1 b -> Term ('SUM a1 b1) b
Curry :: forall {k} {p :: k +-> k} (a :: FBC p) (b1 :: FBC p) (c :: FBC p). (Ob a, Ob b1) => Term ('PROD a b1) c -> Term a ('EXPO b1 c)
Apply :: forall {k} {p :: k +-> k} (a1 :: FBC p) (b :: FBC p). (Ob a1, Ob b) => Term ('PROD ('EXPO a1 b) a1) b

Instances

Instances details

BiCCC k => Promonad (Term :: FBC p -> FBC p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods id :: forall (a :: FBC p). Ob a => Term a a Source Github # (.) :: forall (b :: FBC p) (c :: FBC p) (a :: FBC p). Term b c -> Term a b -> Term a c Source Github #
BiCCC k => MonoidalProfunctor (Term :: FBC p -> FBC p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods one :: Term (Unit :: FBC p) (Unit :: FBC p) Source Github # () :: forall (x1 :: FBC p) (x2 :: FBC p) (y1 :: FBC p) (y2 :: FBC p). Term x1 x2 -> Term y1 y2 -> Term (x1 y1) (x2 ** y2) Source Github #
BiCCC k => Profunctor (Term :: FBC p -> FBC p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods dimap :: forall (c :: FBC p) (a :: FBC p) (b :: FBC p) (d :: FBC p). (c ~> a) -> (b ~> d) -> Term a b -> Term c d Source Github # lmap :: forall (c :: FBC p) (a :: FBC p) (b :: FBC p). (c ~> a) -> Term a b -> Term c b Source Github # rmap :: forall (b :: FBC p) (d :: FBC p) (a :: FBC p). (b ~> d) -> Term a b -> Term a d Source Github # (\\) :: forall (a :: FBC p) (b :: FBC p) r. ((Ob a, Ob b) => r) -> Term a b -> r Source Github #

type family Lower (a :: FBC p) :: k where ... Source Github #

Interpret an object expression as the object of k it denotes.

Equations

Lower ('OBJ x :: FBC p) = x
Lower ('UNIT :: FBC p) = TerminalObject :: k
Lower ('PROD a b :: FBC p) = Lower a && Lower b
Lower ('ZERO :: FBC p) = InitialObject :: k
Lower ('SUM a b :: FBC p) = Lower a \|\| Lower b
Lower ('EXPO a b :: FBC p) = Lower a ~~> Lower b

interp :: forall {k} p (src :: FBC p) (tgt :: FBC p). BiCCC k => (forall (x :: k) (y :: k). p x y -> x ~> y) -> Term src tgt -> Lower src ~> Lower tgt Source Github #

Interpret a Term as the morphism of k it denotes, given an interpretation of the generators, provided k is itself a BiCCC. This is the one place a Term's meaning is pinned down; everything else (including equality) is defined in terms of it.

class KnownFBCOb (a :: FBC p) where Source Github #

Witnesses that an object expression is well-formed by case analysis on its shape.

Methods

fbcCase :: (forall (x :: k). (a ~ ('OBJ x :: FBC p), Ob x) => r) -> (a ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (a ~ 'PROD x y, Ob x, Ob y) => r) -> (a ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (a ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). (a ~ 'EXPO x y, Ob x, Ob y) => r) -> r Source Github #

Instances

Instances details

BiCCC k => KnownFBCOb ('UNIT :: FBC p) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods fbcCase :: (forall (x :: k). (('UNIT :: FBC p) ~ ('OBJ x :: FBC p), Ob x) => r) -> (('UNIT :: FBC p) ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (('UNIT :: FBC p) ~ 'PROD x y, Ob x, Ob y) => r) -> (('UNIT :: FBC p) ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (('UNIT :: FBC p) ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). (('UNIT :: FBC p) ~ 'EXPO x y, Ob x, Ob y) => r) -> r Source Github #
BiCCC k => KnownFBCOb ('ZERO :: FBC p) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods fbcCase :: (forall (x :: k). (('ZERO :: FBC p) ~ ('OBJ x :: FBC p), Ob x) => r) -> (('ZERO :: FBC p) ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (('ZERO :: FBC p) ~ 'PROD x y, Ob x, Ob y) => r) -> (('ZERO :: FBC p) ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). (('ZERO :: FBC p) ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). (('ZERO :: FBC p) ~ 'EXPO x y, Ob x, Ob y) => r) -> r Source Github #
Ob x => KnownFBCOb ('OBJ x :: FBC p) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods fbcCase :: (forall (x0 :: k). (('OBJ x :: FBC p) ~ ('OBJ x0 :: FBC p), Ob x0) => r) -> (('OBJ x :: FBC p) ~ ('UNIT :: FBC p) => r) -> (forall (x1 :: FBC p) (y :: FBC p). (('OBJ x :: FBC p) ~ 'PROD x1 y, Ob x1, Ob y) => r) -> (('OBJ x :: FBC p) ~ ('ZERO :: FBC p) => r) -> (forall (x2 :: FBC p) (y :: FBC p). (('OBJ x :: FBC p) ~ 'SUM x2 y, Ob x2, Ob y) => r) -> (forall (x3 :: FBC p) (y :: FBC p). (('OBJ x :: FBC p) ~ 'EXPO x3 y, Ob x3, Ob y) => r) -> r Source Github #
(BiCCC k, KnownFBCOb a, KnownFBCOb b) => KnownFBCOb ('EXPO a b :: FBC p) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods fbcCase :: (forall (x :: k). ('EXPO a b ~ ('OBJ x :: FBC p), Ob x) => r) -> ('EXPO a b ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). ('EXPO a b ~ 'PROD x y, Ob x, Ob y) => r) -> ('EXPO a b ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). ('EXPO a b ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). ('EXPO a b ~ 'EXPO x y, Ob x, Ob y) => r) -> r Source Github #
(BiCCC k, KnownFBCOb a, KnownFBCOb b) => KnownFBCOb ('PROD a b :: FBC p) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods fbcCase :: (forall (x :: k). ('PROD a b ~ ('OBJ x :: FBC p), Ob x) => r) -> ('PROD a b ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). ('PROD a b ~ 'PROD x y, Ob x, Ob y) => r) -> ('PROD a b ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). ('PROD a b ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). ('PROD a b ~ 'EXPO x y, Ob x, Ob y) => r) -> r Source Github #
(BiCCC k, KnownFBCOb a, KnownFBCOb b) => KnownFBCOb ('SUM a b :: FBC p) Source Github #
Instance details Defined in Proarrow.Category.Instance.FreeBiCCC Methods fbcCase :: (forall (x :: k). ('SUM a b ~ ('OBJ x :: FBC p), Ob x) => r) -> ('SUM a b ~ ('UNIT :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). ('SUM a b ~ 'PROD x y, Ob x, Ob y) => r) -> ('SUM a b ~ ('ZERO :: FBC p) => r) -> (forall (x :: FBC p) (y :: FBC p). ('SUM a b ~ 'SUM x y, Ob x, Ob y) => r) -> (forall (x :: FBC p) (y :: FBC p). ('SUM a b ~ 'EXPO x y, Ob x, Ob y) => r) -> r Source Github #

fbcOb :: forall {k} {p :: k +-> k} (a :: FBC p). (BiCCC k, KnownFBCOb a) => Term a a Source Github #

The identity morphism on a, recovered by case analysis via fbcCase — the only place KnownFBCOb is needed once it's bundled into Ob (see CategoryOf above): everywhere else, an Ob proof in hand is already enough, and obj gives the identity directly.