Copyright | Guillaume Sabbagh 2022 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
A Sketch
is a category equipped with distinguished cones, cocones and tripods. (In litterature, a mixed sketch only distinguishes cones and cocones but we add exponential objects to model second-order logical structures.)
The category is represented by a composition graph.
Synopsis
- type CategorySketch n e = CompositionGraph n e
- type ArrowSketch n e = CGMorphism n e
- type ObjectSketch n e = n
- type ConeSketch n e = Cone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)
- type CoconeSketch n e = Cocone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)
- type TripodSketch n e = Tripod (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)
- data SketchError n e
- = BaseOfConeIsNotInUnderlyingCategory (ConeSketch n e)
- | BaseOfCoconeIsNotInUnderlyingCategory (CoconeSketch n e)
- | BaseOfTripodIsNotInUnderlyingCategory (TripodSketch n e)
- | TripodTwoConeDoesNotBelongToDistinguishedCones (TripodSketch n e)
- | UnderlyingCategoryError (FiniteCategoryError (ArrowSketch n e) (ObjectSketch n e))
- | TwoSameIndexingObjects n
- constructTwoConeFromTripod :: (Eq n, Eq e) => n -> n -> TripodSketch n e -> ConeSketch n e
- constructTwoConeFromTripodText :: TripodSketch Text Text -> ConeSketch Text Text
- data Sketch n e
- underlyingCategory :: Sketch n e -> CategorySketch n e
- supportSketch :: Sketch n e -> Graph n e
- distinguishedCones :: Sketch n e -> Set (ConeSketch n e)
- distinguishedCocones :: Sketch n e -> Set (CoconeSketch n e)
- distinguishedTripods :: Sketch n e -> Set (TripodSketch n e)
- unsafeSketch :: CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Sketch n e
- sketch :: (Eq n, Eq e) => n -> n -> CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Either (SketchError n e) (Sketch n e)
- sketchText :: CategorySketch Text Text -> Set (ConeSketch Text Text) -> Set (CoconeSketch Text Text) -> Set (TripodSketch Text Text) -> Either (SketchError Text Text) (Sketch Text Text)
- checkSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e)
- data SketchMorphism n e
- data SketchMorphismError n e
- = ConeNotSentToACone (ConeSketch n e)
- | CoconeNotSentToACocone (CoconeSketch n e)
- | TripodNotSentToATripod (TripodSketch n e)
- | UnderlyingFunctorError (DiagramError (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e))
- | WrongSource (CategorySketch n e) (CategorySketch n e)
- | WrongTarget (CategorySketch n e) (CategorySketch n e)
- underlyingFunctor :: SketchMorphism n e -> FunctorSketch n e
- unsafeSketchMorphism :: Sketch n e -> Sketch n e -> FunctorSketch n e -> SketchMorphism n e
- sketchMorphism :: (Eq n, Eq e) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Either (SketchMorphismError n e) (SketchMorphism n e)
- canFunctorBePromotedIntoSketchMorphism :: (Eq e, Eq n) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Bool
- data FinSketch n e = FinSketch
- containsLantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
- containsSpotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
- containsCrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
- containsColantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
- containsCospotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
- containsCocrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
- data LightConstruction n e
- = Lantern (ConeSketch n e) (CGMorphism n e) (CGMorphism n e)
- | Spotlight (ConeSketch n e) n n (ConeSketch n e)
- | CrescentMoon (ConeSketch n e) (ConeSketch n e) (Map n n) (ConeSketch n e) n
- | Colantern (CoconeSketch n e) (CGMorphism n e) (CGMorphism n e)
- | Cospotlight (CoconeSketch n e) n n (CoconeSketch n e)
- | CocrescentMoon (CoconeSketch n e) (CoconeSketch n e) (Map n n) (CoconeSketch n e) n
- containsLightConstruction :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
Types for Sketch
type CategorySketch n e = CompositionGraph n e Source #
type ArrowSketch n e = CGMorphism n e Source #
type ObjectSketch n e = n Source #
type ConeSketch n e = Cone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) Source #
type CoconeSketch n e = Cocone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) Source #
type TripodSketch n e = Tripod (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) Source #
data SketchError n e Source #
A SketchError
could be a cone with a base outside the underlying category, a cocone with base outside the underlying category, a tripod with a base outside the underlying category, a tripod where the 2-cone does not belong to the distinguished cones of the sketch or an error in the underlying category.
Instances
constructTwoConeFromTripod :: (Eq n, Eq e) => n -> n -> TripodSketch n e -> ConeSketch n e Source #
constructTwoConeFromTripodText :: TripodSketch Text Text -> ConeSketch Text Text Source #
Specialized version of constructTwoConeFromTripod
for Sketch
of Text
.
Sketch
Sketch is private, use the smart constructor sketch
or unsafeSketch
to construct one. Note that for each distinguished Tripod
, the 2-cone of the Tripod
should belong to the distinguished cones
(the 2-cone can be constructed with constructTwoConeFromTripod
).
Instances
Getters
underlyingCategory :: Sketch n e -> CategorySketch n e Source #
supportSketch :: Sketch n e -> Graph n e Source #
distinguishedCones :: Sketch n e -> Set (ConeSketch n e) Source #
distinguishedCocones :: Sketch n e -> Set (CoconeSketch n e) Source #
distinguishedTripods :: Sketch n e -> Set (TripodSketch n e) Source #
Smart constructors
unsafeSketch :: CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Sketch n e Source #
sketch :: (Eq n, Eq e) => n -> n -> CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Either (SketchError n e) (Sketch n e) Source #
sketchText :: CategorySketch Text Text -> Set (ConeSketch Text Text) -> Set (CoconeSketch Text Text) -> Set (TripodSketch Text Text) -> Either (SketchError Text Text) (Sketch Text Text) Source #
Helpers
checkSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e) Source #
Check wether a Sketch
is well formed or not, return a SketchError
if it is malformed, Nothing otherwise.
Sketch morphism,
data SketchMorphism n e Source #
SketchMorphism is private, use the smart constructor sketchMorphism
or unsafeSketchMorphism
to construct one.
Instances
data SketchMorphismError n e Source #
A SketchError
could be a cone not sent to a cone, a cocone not sent to a cocone or an error in the underlying functor.
ConeNotSentToACone (ConeSketch n e) | |
CoconeNotSentToACocone (CoconeSketch n e) | |
TripodNotSentToATripod (TripodSketch n e) | |
UnderlyingFunctorError (DiagramError (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)) | |
WrongSource (CategorySketch n e) (CategorySketch n e) | |
WrongTarget (CategorySketch n e) (CategorySketch n e) |
Instances
Getter
underlyingFunctor :: SketchMorphism n e -> FunctorSketch n e Source #
Underlying functor of a SketchMorphism
.
Smart constructors
unsafeSketchMorphism :: Sketch n e -> Sketch n e -> FunctorSketch n e -> SketchMorphism n e Source #
Unsafe constructor for a SketchMorphism
. Use with caution, prefer sketch
which checks the structure of the SketchMorphism
.
sketchMorphism :: (Eq n, Eq e) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Either (SketchMorphismError n e) (SketchMorphism n e) Source #
Smart constructor for a SketchMorphism
. It checks wether cones are sent to cones and cocones are sent to cocones.
Other functions
canFunctorBePromotedIntoSketchMorphism :: (Eq e, Eq n) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Bool Source #
Return wether a Functor
can be promoted into a SketchMorphism
.
The category of finite sketches
Instances
Functions for shiny sketches
containsLantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #
containsSpotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #
containsCrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #
Returns a CrescentMoon
found in a Sketch
if it can.
containsColantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #
containsCospotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #
Returns a Cospotlight
found in a Sketch
if it can.
containsCocrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #
Returns a CocrescentMoon
found in a Sketch
if it can.
data LightConstruction n e Source #
A LightConstruction
is either a Lantern
, a Spotlight
, a CrescentMoon
, a Colantern
, a Cospotlight
or a CocrescentMoon
.
A Lantern
is a distinguished cone c1, and two different morphisms m1 m2 such that c1 precomposed with m1 and m2 yield the same cone.
A Spotlight
is a distinguished cone c1, two different indexing objects o1 o2 and a cone c2 such that the legs of c1 at index o1 and o2 are equal and the legs of c2 at index o1 and o2 are different.
A CrescentMoon
is a distinguished cone c1, a distinguished cone c2 such that c1 is contained in c2, a cone c with same base as c1, an indexing object x of the base of c2 not in the base of c1 such that there are at least two arrows from the apex of c to x.
A Colantern
is a distinguished cocone c1, and two different morphisms m1 m2 such that c1 postcomposed with m1 and m2 yield the same cocone.
A Cospotlight
is a distinguished cocone c1, two different indexing objects o1 o2 and a cocone c2 such that the legs of c1 at index o1 and o2 are equal and the legs of c2 at index o1 and o2 are different.
A CocrescentMoon
is a distinguished cocone c1, a distinguished cocone c2 such that c1 is contained in c2, a cocone c with same base as c1, an indexing object x of the base of c2 not in the base of c1 such that there are at least two arrows from x to the nadir of c.
Lantern (ConeSketch n e) (CGMorphism n e) (CGMorphism n e) | |
Spotlight (ConeSketch n e) n n (ConeSketch n e) | |
CrescentMoon (ConeSketch n e) (ConeSketch n e) (Map n n) (ConeSketch n e) n | |
Colantern (CoconeSketch n e) (CGMorphism n e) (CGMorphism n e) | |
Cospotlight (CoconeSketch n e) n n (CoconeSketch n e) | |
CocrescentMoon (CoconeSketch n e) (CoconeSketch n e) (Map n n) (CoconeSketch n e) n |
Instances
containsLightConstruction :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #