Idris2Doc : Stellar.API.Definition

Stellar.API.Definition

(source)
Reexports
import public Stellar.Ops
Definitions
record API : Type
  An API is a pair of a message and a response for that message.

  Totality: total
  Visibility: public export
  Constructor: 
(!>) : (message : Type) -> (message -> Type) -> API

  Projections:
  
.message : API -> Type
  The type of messages we send to the  system.
  
.response : ({rec:0} : API) -> message {rec:0} -> Type
  The type of responses we expect for each message we send.

  Hints:
  
Cartesian mor bi -> APIBifunctor mor bi
  
APIPointed mor f -> APIFunctor mor f
  
APICopointed mor f -> APIFunctor mor f
  
APIMonad mor f -> APIPointed mor f
  
APIComonad mor f -> APIPointed mor f
  
APIAlternative mor bi f -> Cartesian mor bi
  
APIFunctor mor f -> Category mor
  
APIBifunctor mor f -> Category mor
  
APIMonad mor f => Category (APIKleisli f mor)
  
Category (=&>)
  
{auto c : API} -> Functor (Ex c)
  
Preorder API (=&>)
  
Reflexive API (=&>)
  
Transitive API (=&>)
.message : API -> Type
  The type of messages we send to the  system.

  Totality: total
  Visibility: public export
message : API -> Type
  The type of messages we send to the  system.

  Totality: total
  Visibility: public export
.response : ({rec:0} : API) -> message {rec:0} -> Type
  The type of responses we expect for each message we send.

  Totality: total
  Visibility: public export
response : ({rec:0} : API) -> message {rec:0} -> Type
  The type of responses we expect for each message we send.

  Totality: total
  Visibility: public export
Continuation : API -> Type
  Totality: total
  Visibility: public export
(:-) : Type -> Type -> API
  APIs with a constant response type that does not depend on the input
  Also known as a "monomial"

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 0
Through : Type -> API
  The constant interface, returns the input as output.

  Totality: total
  Visibility: public export
End : API
  The leaf interface, neutral for &> and // (composition and tensor)

  Totality: total
  Visibility: public export
Never : API
  The empty interface, neutral for + (coproduct)

  Totality: total
  Visibility: public export
Forever : API
  Nonterminating interface, neutral for * (product)

  Totality: total
  Visibility: public export
(+) : API -> API -> API
  The coproduct on APIs.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 8
(*) : API -> API -> API
  The product of APIs, it uses a product on the messages and a co-product on the responses.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 9
(//) : API -> API -> API
  The tensor on APIs, a product on both message and responses.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
record Ex : API -> Type -> Type
  Extension of a container as a functor.

  Totality: total
  Visibility: public export
  Constructor: 
MkEx : (req : c .message) -> (c .response req -> ty) -> Ex c ty

  Projections:
  
.cont : ({rec:0} : Ex c ty) -> c .response (req {rec:0}) -> ty
  Continuation
  
.req : Ex c ty -> c .message
  Request

  Hint: 
{auto c : API} -> Functor (Ex c)
.req : Ex c ty -> c .message
  Request

  Totality: total
  Visibility: public export
req : Ex c ty -> c .message
  Request

  Totality: total
  Visibility: public export
.cont : ({rec:0} : Ex c ty) -> c .response (req {rec:0}) -> ty
  Continuation

  Totality: total
  Visibility: public export
cont : ({rec:0} : Ex c ty) -> c .response (req {rec:0}) -> ty
  Continuation

  Totality: total
  Visibility: public export
(&>) : API -> API -> API
  Substitution monoidal product, aka composition of APIs.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
(#>) : API -> API -> API
  Continuation monoidal product.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
Lift : (Type -> Type) -> API -> API
  Lifting a functor on types into a functor on APIs

  Totality: total
  Visibility: public export
($-) : (Type -> Type) -> API -> API
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 2
Send : API -> API
  Totality: total
  Visibility: public export