Copyright | (c) 2016 Justus Sagemüller |
---|---|
License | GPL v3 (see COPYING) |
Maintainer | (@) sagemueller $ geo.uni-koeln.de |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
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).
- 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
ReCategory :: k α β -> ReCategory k α β | |
CategoryId :: Object k α => ReCategory k α α | |
CategoryCompo :: Object k β => ReCategory k α β -> ReCategory k β γ -> ReCategory k α γ |
HasAgent k => HasAgent (ReCategory k) Source | |
Category k => Category (ReCategory k) Source | |
Category k => CRCategory (ReCategory k) Source | |
Category k => EnhancedCat (ReCategory k) k Source | |
type SpecificCat (ReCategory k) = k Source | |
type Object (ReCategory k) α = Object k α Source | |
type AgentVal (ReCategory k) α ω = GenericAgent (ReCategory k) α ω Source |
data ReCartesian k α β where Source
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 ((α, β), γ) (α, (β, γ)) |
(HasAgent k, Cartesian k) => HasAgent (ReCartesian k) Source | |
Cartesian k => Cartesian (ReCartesian k) Source | |
Cartesian k => Category (ReCartesian k) Source | |
Cartesian k => CRCartesian (ReCartesian k) Source | |
Cartesian k => CRCategory (ReCartesian k) Source | |
Cartesian k => EnhancedCat (ReCartesian k) k Source | |
type UnitObject (ReCartesian k) = UnitObject k Source | |
type SpecificCat (ReCartesian k) = k Source | |
type Object (ReCartesian k) a = Object k a Source | |
type AgentVal (ReCartesian k) α ω = GenericAgent (ReCartesian k) α ω Source | |
type PairObjects (ReCartesian k) α β = PairObjects k α β Source |
data ReMorphism k α β where Source
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 (α, γ) (β, δ) |
(HasAgent k, Morphism k) => HasAgent (ReMorphism k) Source | |
Morphism k => Cartesian (ReMorphism k) Source | |
Morphism k => Category (ReMorphism k) Source | |
Morphism k => Morphism (ReMorphism k) Source | |
Morphism k => CRMorphism (ReMorphism k) Source | |
Morphism k => CRCartesian (ReMorphism k) Source | |
Morphism k => CRCategory (ReMorphism k) Source | |
Morphism k => EnhancedCat (ReMorphism k) k Source | |
type UnitObject (ReMorphism k) = UnitObject k Source | |
type SpecificCat (ReMorphism k) = k Source | |
type Object (ReMorphism k) a = Object k a Source | |
type AgentVal (ReMorphism k) α ω = GenericAgent (ReMorphism k) α ω Source | |
type PairObjects (ReMorphism k) α β = PairObjects k α β Source |
data RePreArrow k α β where Source
(HasAgent k, PreArrow k) => HasAgent (RePreArrow k) Source | |
PreArrow k => Cartesian (RePreArrow k) Source | |
PreArrow k => Category (RePreArrow k) Source | |
PreArrow k => PreArrow (RePreArrow k) Source | |
PreArrow k => Morphism (RePreArrow k) Source | |
PreArrow k => CRPreArrow (RePreArrow k) Source | |
PreArrow k => CRMorphism (RePreArrow k) Source | |
PreArrow k => CRCartesian (RePreArrow k) Source | |
PreArrow k => CRCategory (RePreArrow k) Source | |
PreArrow k => EnhancedCat (RePreArrow k) k Source | |
type UnitObject (RePreArrow k) = UnitObject k Source | |
type SpecificCat (RePreArrow k) = k Source | |
type Object (RePreArrow k) a = Object k a Source | |
type AgentVal (RePreArrow k) α ω = GenericAgent (RePreArrow k) α ω Source | |
type PairObjects (RePreArrow k) α β = PairObjects k α β Source |
data ReWellPointed k α β where Source