Control.Category.Constrained

Documentation

type O2 k a b = (Obj k a, Obj k b)

type O3 k a b c = (Obj k a, Obj k b, Obj k c)

type O4 k a b c d = (Obj k a, Obj k b, Obj k c, Obj k d)

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...

Equations

All c '[] = ()

All c (x ': xs) = (c x, All c xs)

class Trivial a

Instances

Trivial (a :: k)

Defined in Control.Category.Constrained

ProdObj (Trivial :: Type -> Constraint)

Defined in Control.Category.Constrained

Methods

prodobj :: (Trivial a, Trivial b) => Dict (Trivial (a ⊗ b))

objprod :: (z ~ (a ⊗ b), Trivial z) => Dict (Trivial a, Trivial b)

objunit :: Dict (Trivial ())

class Category k where

Associated Types

type Obj k :: Type -> Constraint

type Obj k = Trivial

Methods

id :: Obj k a => a `k` a

(∘) :: (Obj k a, Obj k b, Obj k c) => (b `k` c) -> (a `k` b) -> a `k` c infixl 8

Instances

Category (FUN x :: Type -> Type -> Type)

Defined in Control.Category.Constrained

Associated Types

type Obj (FUN x) :: Type -> Constraint

Methods

id :: Obj (FUN x) a => FUN x a a

(∘) :: (Obj (FUN x) a, Obj (FUN x) b, Obj (FUN x) c) => FUN x b c -> FUN x a b -> FUN x a c

(.) :: (Category k, O3 k a b c) => k b c -> k a b -> k a c infixl 8

class ProdObj con where

Methods

prodobj :: (con a, con b) => Dict (con (a ⊗ b))

objprod :: forall z a b. (z ~ (a ⊗ b), con z) => Dict (con a, con b)

objunit :: Dict (con ())

Instances

ProdObj (Trivial :: Type -> Constraint)

Defined in Control.Category.Constrained

Methods

prodobj :: (Trivial a, Trivial b) => Dict (Trivial (a ⊗ b))

objprod :: (z ~ (a ⊗ b), Trivial z) => Dict (Trivial a, Trivial b)

objunit :: Dict (Trivial ())

objProd :: forall k a b z. (z ~ (a ⊗ b), Obj k z, Monoidal k) => Dict (Obj k a, Obj k b)

prodObj :: forall k a b. (Monoidal k, Obj k a, Obj k b) => Dict (Obj k (a ⊗ b))

unitObj :: forall k. Monoidal k => Dict (Obj k ())

(//) :: Dict c -> (c => k) -> k infixr 0

type (⊗) a b = (a, b) infixr 7

class (ProdObj (Obj k), Category k) => Monoidal k where

Methods

(×) :: (Obj k a, Obj k b, Obj k c, Obj k d) => (a `k` b) -> (c `k` d) -> (a ⊗ c) `k` (b ⊗ d)

swap :: (Obj k a, Obj k b) => (a ⊗ b) `k` (b ⊗ a)

assoc :: (Obj k a, Obj k b, Obj k c) => ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))

assoc' :: (Obj k a, Obj k b, Obj k c) => (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)

unitor :: Obj k a => a `k` (a ⊗ ())

unitor' :: Obj k a => (a ⊗ ()) `k` a

Instances

Monoidal (FUN m :: Type -> Type -> Type)

Defined in Control.Category.Constrained

Methods

(×) :: (Obj (FUN m) a, Obj (FUN m) b, Obj (FUN m) c, Obj (FUN m) d) => FUN m a b -> FUN m c d -> FUN m (a ⊗ c) (b ⊗ d)

swap :: (Obj (FUN m) a, Obj (FUN m) b) => FUN m (a ⊗ b) (b ⊗ a)

assoc :: (Obj (FUN m) a, Obj (FUN m) b, Obj (FUN m) c) => FUN m ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))

assoc' :: (Obj (FUN m) a, Obj (FUN m) b, Obj (FUN m) c) => FUN m (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)

unitor :: Obj (FUN m) a => FUN m a (a ⊗ ())

unitor' :: Obj (FUN m) a => FUN m (a ⊗ ()) a

class Monoidal k => Cartesian k where

Minimal complete definition

exl, exr, dup | exl, exr, (▵) | dis, dup | dis, (▵)

Methods

exl :: forall a b. O2 k a b => (a ⊗ b) `k` a

exr :: forall a b. O2 k a b => (a ⊗ b) `k` b

dis :: forall a. Obj k a => a `k` ()

dup :: (Obj k a, Obj k (a ⊗ a)) => a `k` (a ⊗ a)

(▵) :: forall a b c. (Obj k a, Obj k b, Obj k c) => (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)

Instances

Cartesian (->)

Defined in Control.Category.Constrained

Methods

exl :: O2 (->) a b => (a ⊗ b) -> a

exr :: O2 (->) a b => (a ⊗ b) -> b

dis :: Obj (->) a => a -> ()

dup :: (Obj (->) a, Obj (->) (a ⊗ a)) => a -> (a ⊗ a)

(▵) :: (Obj (->) a, Obj (->) b, Obj (->) c) => (a -> b) -> (a -> c) -> a -> (b ⊗ c)

disDefault :: forall k a. (Cartesian k, Obj k a) => a `k` ()

exlDefault :: forall k a b. (Cartesian k, O2 k a b) => (a ⊗ b) `k` a

exrDefault :: forall k a b. (Cartesian k, O2 k a b) => (a ⊗ b) `k` b

(▵!) :: forall k a b c. (Cartesian k, O3 k a b c) => (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)

cartesianCross :: (Obj k (b1 ⊗ b2), Obj k b3, Obj k c, Obj k b1, Obj k b2, Cartesian k) => k b1 b3 -> k b2 c -> k (b1 ⊗ b2) (b3 ⊗ c)

cartesianUnitor :: forall a k. (Obj k a, Obj k (), Cartesian k) => a `k` (a ⊗ ())

cartesianUnitor' :: forall a k. (Obj k a, Obj k (), Cartesian k) => (a ⊗ ()) `k` a

cartesianSwap :: forall a b k. (Obj k a, Obj k b, Cartesian k) => (a ⊗ b) `k` (b ⊗ a)

cartesianAssoc :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))

cartesianAssoc' :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)

class Monoidal k => CoCartesian k where

Minimal complete definition

inl, inr

Methods

inl :: O2 k a b => a `k` (a ⊗ b)

inr :: O2 k a b => b `k` (a ⊗ b)

new :: forall a. Obj k a => () `k` a

jam :: Obj k a => (a ⊗ a) `k` a

(▿) :: forall a b c. (Obj k a, Obj k b, Obj k c) => (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a

jamDefault :: (Obj k a, CoCartesian k) => (a ⊗ a) `k` a

newDefault :: forall k a. (Obj k a, CoCartesian k) => () `k` a

(▿!) :: forall k a b c. (O3 k a b c, CoCartesian k) => (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a

transp :: forall a b c d k con. (con ~ Obj k, Monoidal k, O4 k a b c d, forall α β. (con α, con β) => con (α, β)) => ((a, b) ⊗ (c, d)) `k` ((a, c) ⊗ (b, d))

class Cartesian k => Closed k where

Methods

apply :: O2 k a b => ((a -> b) ⊗ a) `k` b

curry :: O3 k a b c => ((a ⊗ b) `k` c) -> a `k` (b -> c)

Instances

Closed (->)

Defined in Control.Category.Constrained

Methods

apply :: O2 (->) a b => ((a -> b) ⊗ a) -> b

curry :: O3 (->) a b c => ((a ⊗ b) -> c) -> a -> (b -> c)

class Invertible k where

Methods

dual :: (a `k` b) -> b `k` a

type Hopf k = (Cartesian k, CoCartesian k)

type Comparator k = forall a b b'. k a b -> k a b' -> Maybe (b :~: b')

class Category k => HasCompare k where

Methods

compareMorphs :: Comparator k

data Order a b where

Equality-witnessing order type

Constructors

LT, GT :: Order a b

EQ :: Order a a