Control.Category.Constrained.Reified

GADTs that mirror the class hierarchy from Category to (at the moment) Cartesian, reifying all the available “free” composition operations.

These can be used as a “trivial base case“ for all kinds of categories: it turns out these basic operations are often not so trivial to implement, or only possible with stronger constraints than you'd like. For instance, the category of affine mappings can only be implemented directly as a category on vector spaces, because the identity mapping has zero constant offset.

By leaving the free compositions reified to runtime syntax trees, this problem can be avoided. In other applications, you may not need these cases, but can still benefit from them for optimisation (composition with id is always trivial, and so on).

Reified versions of the category classes

data ReCategory k α β where

Constructors

ReCategory :: k α β -> ReCategory k α β

CategoryId :: Object k α => ReCategory k α α

CategoryCompo :: Object k β => ReCategory k α β -> ReCategory k β γ -> ReCategory k α γ

Instances

HasAgent k => HasAgent (ReCategory k)

Category k => Category (ReCategory k)

Category k => CRCategory (ReCategory k)

Category k => EnhancedCat (ReCategory k) k

type SpecificCat (ReCategory k) = k

type Object (ReCategory k) α = Object k α

type AgentVal (ReCategory k) α ω = GenericAgent (ReCategory k) α ω

data ReCartesian k α β where

Constructors

ReCartesian :: k α β -> ReCartesian k α β

CartesianId :: Object k α => ReCartesian k α α

CartesianCompo :: Object k β => ReCartesian k α β -> ReCartesian k β γ -> ReCartesian k α γ

CartesianSwap :: (ObjectPair k α β, ObjectPair k β α) => ReCartesian k (α, β) (β, α)

CartesianAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReCartesian k α (α, u)

CartesianDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReCartesian k (α, u) α

CartesianRegroup :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => ReCartesian k (α, (β, γ)) ((α, β), γ)

CartesianRegroup_ :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => ReCartesian k ((α, β), γ) (α, (β, γ))

Instances

(HasAgent k, Cartesian k) => HasAgent (ReCartesian k)

Cartesian k => Cartesian (ReCartesian k)

Cartesian k => Category (ReCartesian k)

Cartesian k => CRCartesian (ReCartesian k)

Cartesian k => CRCategory (ReCartesian k)

Cartesian k => EnhancedCat (ReCartesian k) k

type UnitObject (ReCartesian k) = UnitObject k

type SpecificCat (ReCartesian k) = k

type Object (ReCartesian k) a = Object k a

type AgentVal (ReCartesian k) α ω = GenericAgent (ReCartesian k) α ω

type PairObjects (ReCartesian k) α β = PairObjects k α β

data ReMorphism k α β where

Constructors

ReMorphism :: k α β -> ReMorphism k α β

MorphismId :: Object k α => ReMorphism k α α

MorphismCompo :: Object k β => ReMorphism k α β -> ReMorphism k β γ -> ReMorphism k α γ

MorphismSwap :: (ObjectPair k α β, ObjectPair k β α) => ReMorphism k (α, β) (β, α)

MorphismAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReMorphism k α (α, u)

MorphismDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReMorphism k (α, u) α

MorphismRegroup :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => ReMorphism k (α, (β, γ)) ((α, β), γ)

MorphismRegroup_ :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => ReMorphism k ((α, β), γ) (α, (β, γ))

MorphismPar :: (ObjectPair k α γ, ObjectPair k β δ) => ReMorphism k α β -> ReMorphism k γ δ -> ReMorphism k (α, γ) (β, δ)

Instances

(HasAgent k, Morphism k) => HasAgent (ReMorphism k)

Morphism k => Cartesian (ReMorphism k)

Morphism k => Category (ReMorphism k)

Morphism k => Morphism (ReMorphism k)

Morphism k => CRMorphism (ReMorphism k)

Morphism k => CRCartesian (ReMorphism k)

Morphism k => CRCategory (ReMorphism k)

Morphism k => EnhancedCat (ReMorphism k) k

type UnitObject (ReMorphism k) = UnitObject k

type SpecificCat (ReMorphism k) = k

type Object (ReMorphism k) a = Object k a

type AgentVal (ReMorphism k) α ω = GenericAgent (ReMorphism k) α ω

type PairObjects (ReMorphism k) α β = PairObjects k α β

data RePreArrow k α β where

Constructors

RePreArrow :: k α β -> RePreArrow k α β

PreArrowId :: Object k α => RePreArrow k α α

PreArrowCompo :: Object k β => RePreArrow k α β -> RePreArrow k β γ -> RePreArrow k α γ

PreArrowSwap :: (ObjectPair k α β, ObjectPair k β α) => RePreArrow k (α, β) (β, α)

PreArrowAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => RePreArrow k α (α, u)

PreArrowDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => RePreArrow k (α, u) α

PreArrowRegroup :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => RePreArrow k (α, (β, γ)) ((α, β), γ)

PreArrowRegroup_ :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => RePreArrow k ((α, β), γ) (α, (β, γ))

PreArrowPar :: (ObjectPair k α γ, ObjectPair k β δ) => RePreArrow k α β -> RePreArrow k γ δ -> RePreArrow k (α, γ) (β, δ)

PreArrowFanout :: (Object k α, ObjectPair k β γ) => RePreArrow k α β -> RePreArrow k α γ -> RePreArrow k α (β, γ)

PreArrowTerminal :: Object k α => RePreArrow k α (UnitObject k)

PreArrowFst :: ObjectPair k α β => RePreArrow k (α, β) α

PreArrowSnd :: ObjectPair k α β => RePreArrow k (α, β) β

Instances

(HasAgent k, PreArrow k) => HasAgent (RePreArrow k)

PreArrow k => Cartesian (RePreArrow k)

PreArrow k => Category (RePreArrow k)

PreArrow k => PreArrow (RePreArrow k)

PreArrow k => Morphism (RePreArrow k)

PreArrow k => CRPreArrow (RePreArrow k)

PreArrow k => CRMorphism (RePreArrow k)

PreArrow k => CRCartesian (RePreArrow k)

PreArrow k => CRCategory (RePreArrow k)

PreArrow k => EnhancedCat (RePreArrow k) k

type UnitObject (RePreArrow k) = UnitObject k

type SpecificCat (RePreArrow k) = k

type Object (RePreArrow k) a = Object k a

type AgentVal (RePreArrow k) α ω = GenericAgent (RePreArrow k) α ω

type PairObjects (RePreArrow k) α β = PairObjects k α β

data ReWellPointed k α β where

Constructors

ReWellPointed :: k α β -> ReWellPointed k α β

WellPointedId :: Object k α => ReWellPointed k α α

WellPointedCompo :: Object k β => ReWellPointed k α β -> ReWellPointed k β γ -> ReWellPointed k α γ

WellPointedSwap :: (ObjectPair k α β, ObjectPair k β α) => ReWellPointed k (α, β) (β, α)

WellPointedAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReWellPointed k α (α, u)

WellPointedDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReWellPointed k (α, u) α

WellPointedRegroup :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => ReWellPointed k (α, (β, γ)) ((α, β), γ)

WellPointedRegroup_ :: (ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ), ObjectPair k (α, β) γ) => ReWellPointed k ((α, β), γ) (α, (β, γ))

WellPointedPar :: (ObjectPair k α γ, ObjectPair k β δ) => ReWellPointed k α β -> ReWellPointed k γ δ -> ReWellPointed k (α, γ) (β, δ)

WellPointedFanout :: (Object k α, ObjectPair k β γ) => ReWellPointed k α β -> ReWellPointed k α γ -> ReWellPointed k α (β, γ)

WellPointedTerminal :: Object k α => ReWellPointed k α (UnitObject k)

WellPointedFst :: ObjectPair k α β => ReWellPointed k (α, β) α

WellPointedSnd :: ObjectPair k α β => ReWellPointed k (α, β) β

WellPointedConst :: (Object k ν, ObjectPoint k α) => α -> ReWellPointed k ν α

Instances

(HasAgent k, WellPointed k) => HasAgent (ReWellPointed k)

WellPointed k => Cartesian (ReWellPointed k)

WellPointed k => Category (ReWellPointed k)

WellPointed k => WellPointed (ReWellPointed k)

WellPointed k => PreArrow (ReWellPointed k)

WellPointed k => Morphism (ReWellPointed k)

WellPointed k => CRWellPointed (ReWellPointed k)

WellPointed k => CRPreArrow (ReWellPointed k)

WellPointed k => CRMorphism (ReWellPointed k)

WellPointed k => CRCartesian (ReWellPointed k)

WellPointed k => CRCategory (ReWellPointed k)

WellPointed k => EnhancedCat (ReWellPointed k) k

type UnitObject (ReWellPointed k) = UnitObject k

type SpecificCat (ReWellPointed k) = k

type Object (ReWellPointed k) a = Object k a

type PointObject (ReWellPointed k) α = PointObject k α

type AgentVal (ReWellPointed k) α ω = GenericAgent (ReWellPointed k) α ω

type PairObjects (ReWellPointed k) α β = PairObjects k α β