Idris2Doc : Stellar.API.Interface

Stellar.API.Interface

(source)
Reexports
import public Control.Relation
import public Control.Category
Definitions
interface APIFunctor : Rel API -> (API -> API) -> Type
  Parameters: mor, f
Constraints: Category mor
Constructor: 
MkAPIFunctor

Methods:
  
map : mor a b -> mor (f a) (f b)

Implementations:
  
APIFunctor (=&>) Maybe
  
APIFunctor (=&>) Maybe
map : APIFunctor mor f => mor a b -> mor (f a) (f b)
  Totality: total
  Visibility: public export
interface APIBifunctor : Rel API -> (API -> API -> API) -> Type
  Parameters: mor, f
Constraints: Category mor
Constructor: 
MkAPIBifunctor

Methods:
  
bimap : mor a b -> mor x y -> mor (f a x) (f b y)

Implementation: 
APIBifunctor (=&>) (*)
bimap : APIBifunctor mor f => mor a b -> mor x y -> mor (f a x) (f b y)
  Totality: total
  Visibility: public export
mapFst : APIBifunctor mor bi => mor a b -> mor (bi a c) (bi b c)
  Totality: total
  Visibility: export
mapSnd : APIBifunctor mor bi => mor a b -> mor (bi c a) (bi c b)
  Totality: total
  Visibility: export
interface APIMonoid : Rel API -> (API -> API -> API) -> Type
  Parameters: mor, bi
Methods:
  
empty : API
  
idLeft : mor (bi empty a) a
  
idRight : mor (bi a empty) a
  
assoc1 : mor (bi a (bi b c)) (bi (bi a b) c)
  
assoc2 : mor (bi (bi a b) c) (bi a (bi b c))
empty : APIMonoid mor bi => API
  Totality: total
  Visibility: public export
idLeft : {auto __con : APIMonoid mor bi} -> mor (bi empty a) a
  Totality: total
  Visibility: public export
idRight : {auto __con : APIMonoid mor bi} -> mor (bi a empty) a
  Totality: total
  Visibility: public export
assoc1 : APIMonoid mor bi => mor (bi a (bi b c)) (bi (bi a b) c)
  Totality: total
  Visibility: public export
assoc2 : APIMonoid mor bi => mor (bi (bi a b) c) (bi a (bi b c))
  Totality: total
  Visibility: public export
interface Cartesian : Rel API -> (API -> API -> API) -> Type
  Parameters: mor, bi
Constraints: APIBifunctor mor bi
Constructor: 
MkAPICartesian

Methods:
  
fst : mor (bi a b) a
  
snd : mor (bi a b) b
  
(&&&) : mor c a -> mor c b -> mor c (bi a b)

Implementation: 
Cartesian (=&>) (*)
fst : Cartesian mor bi => mor (bi a b) a
  Totality: total
  Visibility: public export
snd : Cartesian mor bi => mor (bi a b) b
  Totality: total
  Visibility: public export
(&&&) : Cartesian mor bi => mor c a -> mor c b -> mor c (bi a b)
  Totality: total
  Visibility: public export
swap : Cartesian mor bi => mor (bi x y) (bi y x)
  Totality: total
  Visibility: export
duplicate : Cartesian mor bi => mor a (bi a a)
  Totality: total
  Visibility: export
assocCart1 : Cartesian mor bi => mor (bi a (bi b c)) (bi (bi a b) c)
  Totality: total
  Visibility: export
assocCart2 : Cartesian mor bi => mor (bi (bi a b) c) (bi a (bi b c))
  Totality: total
  Visibility: export
interface APIAlternative : Rel API -> (API -> API -> API) -> (API -> API) -> Type
  Parameters: mor, bi, f
Constraints: Cartesian mor bi
Constructor: 
MkAPIAlternative

Methods:
  
err : mor Forever (f a)
  
firstSuccess : mor (bi (f a) (f a)) (f a)

Implementation: 
APIAlternative (=&>) (*) Maybe
err : APIAlternative mor bi f => mor Forever (f a)
  Totality: total
  Visibility: public export
firstSuccess : APIAlternative mor bi f => mor (bi (f a) (f a)) (f a)
  Totality: total
  Visibility: public export
or : APIAlternative mor bi f => mor a (f b) -> mor a (f b) -> mor a (f b)
  Totality: total
  Visibility: export
tryAll : APIAlternative mor bi f => List1 (mor a (f b)) -> mor a (f b)
  Totality: total
  Visibility: export
interface APIPointed : (API -> API -> Type) -> (API -> API) -> Type
  Parameters: mor, f
Constraints: APIFunctor mor f
Constructor: 
MkAPIPointed

Methods:
  
pure : mor a (f a)

Implementations:
  
APIPointed (=&>) Maybe
  
APIPointed (=&>) Maybe
pure : APIPointed mor f => mor a (f a)
  Totality: total
  Visibility: public export
interface APIMonad : (API -> API -> Type) -> (API -> API) -> Type
  Parameters: mor, f
Constraints: APIPointed mor f
Constructor: 
MkAPIMonad

Methods:
  
join : mor (f (f a)) (f a)

Implementations:
  
APIMonad (=&>) Maybe
  
APIMonad (=&>) Maybe
join : APIMonad mor f => mor (f (f a)) (f a)
  Totality: total
  Visibility: public export
interface APICopointed : (API -> API -> Type) -> (API -> API) -> Type
  Parameters: mor, f
Constraints: APIFunctor mor f
Constructor: 
MkAPICopointed

Methods:
  
extract : mor (f a) a
extract : APICopointed mor f => mor (f a) a
  Totality: total
  Visibility: public export
interface APIComonad : (API -> API -> Type) -> (API -> API) -> Type
  Parameters: mor, f
Constraints: APIPointed mor f
Constructor: 
MkAPIComonad

Methods:
  
dup : mor (f a) (f (f a))
dup : APIComonad mor f => mor (f a) (f (f a))
  Totality: total
  Visibility: public export
returnFirst : APIAlternative mor bi f => mor a (f b) -> mor a (f b) -> mor a (f b)
  Totality: total
  Visibility: export
(>=>) : APIMonad mor f => mor a (f b) -> mor b (f c) -> mor a (f c)
  Kleisli composition

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(<=<) : APIComonad mor f => mor (f a) b -> mor (f b) c -> mor (f a) c
  Cokleisli composition, NOT right-to-left kleisli composition

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
APIKleisli : (API -> API) -> Rel API -> Rel API
  Totality: total
  Visibility: public export
APIKleisliInstance : APIMonad mor f => Category (APIKleisli f mor)
  Totality: total
  Visibility: export