proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Instance.List

Synopsis
  • data LIST k = L [k]
  • data List (as :: LIST k) (bs :: LIST k) where
    • Nil :: forall {k}. List ('L ('[] :: [k])) ('L ('[] :: [k]))
    • Cons :: forall {k} (as1 :: [k]) (bs1 :: [k]) (a :: k) (b :: k). (IsList as1, IsList bs1) => (a ~> b) -> List ('L as1) ('L bs1) -> List ('L (a ': as1)) ('L (b ': bs1))
  • mkCons :: forall k (a :: k) (b :: k) (as :: [k]) (bs :: [k]). CategoryOf k => (a ~> b) -> ('L as ~> 'L bs) -> 'L (a ': as) ~> 'L (b ': bs)
  • class ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => Assoc (as :: [k]) (bs :: [k]) (cs :: [k])
  • class (as ~ (as ++ ('[] :: [k])), forall (bs :: [k]) (cs :: [k]). Assoc as bs cs) => IsList (as :: [k]) where

Documentation

data LIST k Source Comments #

Constructors

L [k] 

Instances

Instances details
CategoryOf k => Monoidal (LIST k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Instance.List

type Unit = 'L ('[] :: [k])

Methods

withOb2 :: forall (a :: LIST k) (b :: LIST k) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Comments #

leftUnitor :: forall (a :: LIST k). Ob a => ((Unit :: LIST k) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: LIST k). Ob a => a ~> ((Unit :: LIST k) ** a) Source Comments #

rightUnitor :: forall (a :: LIST k). Ob a => (a ** (Unit :: LIST k)) ~> a Source Comments #

rightUnitorInv :: forall (a :: LIST k). Ob a => a ~> (a ** (Unit :: LIST k)) Source Comments #

associator :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: LIST k) (b :: LIST k) (c :: LIST k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

CategoryOf k => CategoryOf (LIST k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.List

type (~>) = List :: LIST k -> LIST k -> Type
CategoryOf k => Promonad (List :: LIST k -> LIST k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

id :: forall (a :: LIST k). Ob a => List a a Source Comments #

(.) :: forall (b :: LIST k) (c :: LIST k) (a :: LIST k). List b c -> List a b -> List a c Source Comments #

CategoryOf k => MonoidalProfunctor (List :: LIST k -> LIST k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

par0 :: List (Unit :: LIST k) (Unit :: LIST k) Source Comments #

par :: forall (x1 :: LIST k) (x2 :: LIST k) (y1 :: LIST k) (y2 :: LIST k). List x1 x2 -> List y1 y2 -> List (x1 ** y1) (x2 ** y2) Source Comments #

CategoryOf k => Profunctor (List :: LIST k -> LIST k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

dimap :: forall (c :: LIST k) (a :: LIST k) (b :: LIST k) (d :: LIST k). (c ~> a) -> (b ~> d) -> List a b -> List c d Source Comments #

(\\) :: forall (a :: LIST k) (b :: LIST k) r. ((Ob a, Ob b) => r) -> List a b -> r Source Comments #

type Unit Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

type Unit = 'L ('[] :: [k])
type (~>) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

type (~>) = List :: LIST k -> LIST k -> Type
type Ob (as :: LIST k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

type Ob (as :: LIST k) = (Is ('L :: [k] -> LIST k) as, IsList (UN ('L :: [k] -> LIST k) as))
type (p :: LIST k) ** (q :: LIST k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

type (p :: LIST k) ** (q :: LIST k) = 'L (UN ('L :: [k] -> LIST k) p ++ UN ('L :: [k] -> LIST k) q)
type UN ('L :: [k] -> LIST k) ('L as :: LIST k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

type UN ('L :: [k] -> LIST k) ('L as :: LIST k) = as

data List (as :: LIST k) (bs :: LIST k) where Source Comments #

The free monoid in CAT

Constructors

Nil :: forall {k}. List ('L ('[] :: [k])) ('L ('[] :: [k])) 
Cons :: forall {k} (as1 :: [k]) (bs1 :: [k]) (a :: k) (b :: k). (IsList as1, IsList bs1) => (a ~> b) -> List ('L as1) ('L bs1) -> List ('L (a ': as1)) ('L (b ': bs1)) 

Instances

Instances details
CategoryOf k => Promonad (List :: LIST k -> LIST k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

id :: forall (a :: LIST k). Ob a => List a a Source Comments #

(.) :: forall (b :: LIST k) (c :: LIST k) (a :: LIST k). List b c -> List a b -> List a c Source Comments #

CategoryOf k => MonoidalProfunctor (List :: LIST k -> LIST k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

par0 :: List (Unit :: LIST k) (Unit :: LIST k) Source Comments #

par :: forall (x1 :: LIST k) (x2 :: LIST k) (y1 :: LIST k) (y2 :: LIST k). List x1 x2 -> List y1 y2 -> List (x1 ** y1) (x2 ** y2) Source Comments #

CategoryOf k => Profunctor (List :: LIST k -> LIST k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

dimap :: forall (c :: LIST k) (a :: LIST k) (b :: LIST k) (d :: LIST k). (c ~> a) -> (b ~> d) -> List a b -> List c d Source Comments #

(\\) :: forall (a :: LIST k) (b :: LIST k) r. ((Ob a, Ob b) => r) -> List a b -> r Source Comments #

mkCons :: forall k (a :: k) (b :: k) (as :: [k]) (bs :: [k]). CategoryOf k => (a ~> b) -> ('L as ~> 'L bs) -> 'L (a ': as) ~> 'L (b ': bs) Source Comments #

class ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => Assoc (as :: [k]) (bs :: [k]) (cs :: [k]) Source Comments #

Instances

Instances details
(as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs) => Assoc (as :: [k]) (bs :: [k]) (cs :: [k]) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

class (as ~ (as ++ ('[] :: [k])), forall (bs :: [k]) (cs :: [k]). Assoc as bs cs) => IsList (as :: [k]) where Source Comments #

Methods

listId :: List ('L as) ('L as) Source Comments #

withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList (as ++ bs) => r) -> r Source Comments #

Instances

Instances details
IsList ('[] :: [k]) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

listId :: List ('L ('[] :: [k])) ('L ('[] :: [k])) Source Comments #

withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList (('[] :: [k]) ++ bs) => r) -> r Source Comments #

(CategoryOf k, Ob a, IsList as) => IsList (a ': as :: [k]) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.List

Methods

listId :: List ('L (a ': as)) ('L (a ': as)) Source Comments #

withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList ((a ': as) ++ bs) => r) -> r Source Comments #