| Copyright | (c) 2016 Justus Sagemüller |
|---|---|
| License | GPL v3 (see COPYING) |
| Maintainer | (@) sagemueller $ geo.uni-koeln.de |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Control.Category.Constrained.Reified
Description
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).
Synopsis
- data ReCategory (k :: * -> * -> *) (α :: *) (β :: *) where
- ReCategory :: k α β -> ReCategory k α β
- CategoryId :: Object k α => ReCategory k α α
- CategoryCompo :: Object k β => ReCategory k α β -> ReCategory k β γ -> ReCategory k α γ
- data ReCartesian (k :: * -> * -> *) (α :: *) (β :: *) where
- 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 ((α, β), γ) (α, (β, γ))
- data ReMorphism (k :: * -> * -> *) (α :: *) (β :: *) where
- 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 (α, γ) (β, δ)
- data RePreArrow (k :: * -> * -> *) (α :: *) (β :: *) where
- 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 (α, β) β
- data ReWellPointed (k :: * -> * -> *) (α :: *) (β :: *) where
- 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 ν α
Reified versions of the category classes
data ReCategory (k :: * -> * -> *) (α :: *) (β :: *) where Source #
Constructors
| ReCategory :: k α β -> ReCategory k α β | |
| CategoryId :: Object k α => ReCategory k α α | |
| CategoryCompo :: Object k β => ReCategory k α β -> ReCategory k β γ -> ReCategory k α γ |
Instances
data ReCartesian (k :: * -> * -> *) (α :: *) (β :: *) where Source #
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
data ReMorphism (k :: * -> * -> *) (α :: *) (β :: *) where Source #
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
data RePreArrow (k :: * -> * -> *) (α :: *) (β :: *) where Source #
Constructors
Instances
data ReWellPointed (k :: * -> * -> *) (α :: *) (β :: *) where Source #
Constructors