linear-smc-2.0.1: Build SMC morphisms using linear types
Safe HaskellSafe-Inferred
LanguageHaskell2010

Control.Category.Constrained

Synopsis

Documentation

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

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

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

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

Equations

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

class Trivial a Source #

Instances

Instances details
Trivial (a :: k) Source # 
Instance details

Defined in Control.Category.Constrained

ProdObj (Trivial :: Type -> Constraint) Source # 
Instance details

Defined in Control.Category.Constrained

Methods

prodobj :: (Trivial a, Trivial b) => Dict (Trivial (a b)) Source #

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

objunit :: Dict (Trivial ()) Source #

class Category k where Source #

Associated Types

type Obj k :: Type -> Constraint Source #

type Obj k = Trivial

Methods

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

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

Instances

Instances details
Category (FUN x :: TYPE LiftedRep -> TYPE LiftedRep -> Type) Source # 
Instance details

Defined in Control.Category.Constrained

Associated Types

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

Methods

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

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

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

class ProdObj con where Source #

Methods

prodobj :: (con a, con b) => Dict (con (a b)) Source #

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

objunit :: Dict (con ()) Source #

Instances

Instances details
ProdObj (Trivial :: Type -> Constraint) Source # 
Instance details

Defined in Control.Category.Constrained

Methods

prodobj :: (Trivial a, Trivial b) => Dict (Trivial (a b)) Source #

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

objunit :: Dict (Trivial ()) Source #

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

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

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

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

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

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

Methods

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

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

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

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

unitor :: Obj k a => a `k` (a ()) Source #

unitor' :: Obj k a => (a ()) `k` a Source #

Instances

Instances details
Monoidal (FUN m :: TYPE LiftedRep -> TYPE LiftedRep -> Type) Source # 
Instance details

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) Source #

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

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

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

unitor :: Obj (FUN m) a => FUN m a (a ()) Source #

unitor' :: Obj (FUN m) a => FUN m (a ()) a Source #

class Monoidal k => Cartesian k where Source #

Minimal complete definition

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

Methods

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

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

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

dup :: (Obj k a, Obj k (a a)) => a `k` (a a) Source #

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

Instances

Instances details
Cartesian (->) Source # 
Instance details

Defined in Control.Category.Constrained

Methods

exl :: O2 (->) a b => (a b) -> a Source #

exr :: O2 (->) a b => (a b) -> b Source #

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

dup :: (Obj (->) a, Obj (->) (a a)) => a -> (a a) Source #

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

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

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

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

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

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) Source #

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

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

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

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

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

class Monoidal k => CoCartesian k where Source #

Minimal complete definition

inl, inr

Methods

inl :: O2 k a b => a `k` (a b) Source #

inr :: O2 k a b => b `k` (a b) Source #

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

jam :: Obj k a => (a a) `k` a Source #

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

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

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

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

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)) Source #

class Cartesian k => Closed k where Source #

Methods

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

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

Instances

Instances details
Closed (->) Source # 
Instance details

Defined in Control.Category.Constrained

Methods

apply :: O2 (->) a b => ((a -> b) a) -> b Source #

curry :: O3 (->) a b c => ((a b) -> c) -> a -> (b -> c) Source #

class Invertible k where Source #

Methods

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

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

class Category k => HasCompare k where Source #

data Order a b where Source #

Equality-witnessing order type

Constructors

LT, GT :: Order a b 
EQ :: Order a a