0 | module Stellar.API.Definition
  1 |
  2 | import public Stellar.Ops
  3 | import Data.Sigma
  4 | import Data.Product
  5 | import Data.Coproduct
  6 |
  7 | ||| An API is a pair of a message and a response for that message.
  8 | public export
  9 | record API where
 10 |   constructor (!>)
 11 |   ||| The type of messages we send to the  system.
 12 |   message : Type
 13 |   ||| The type of responses we expect for each message we send.
 14 |   response : message -> Type
 15 |
 16 | %pair API message response
 17 |
 18 | %name API msg, res
 19 |
 20 | public export
 21 | Continuation : API -> Type
 22 | Continuation a = (x : a.message) -> a.response x
 23 |
 24 | ||| APIs with a constant response type that does not depend on the input
 25 | ||| Also known as a "monomial"
 26 | public export
 27 | (:-) : Type -> Type -> API
 28 | (:-) ty sy = (x : ty) !> sy
 29 |
 30 | ||| The constant interface, returns the input as output.
 31 | public export
 32 | Through : Type -> API
 33 | Through ty = ty :- ty
 34 |
 35 | ||| The leaf interface, neutral for &> and // (composition and tensor)
 36 | public export
 37 | End : API
 38 | End = Unit :- Unit
 39 |
 40 | ||| The empty interface, neutral for + (coproduct)
 41 | public export
 42 | Never : API
 43 | Never = Void :- Void
 44 |
 45 | ||| Nonterminating interface, neutral for * (product)
 46 | public export
 47 | Forever : API
 48 | Forever = Unit :- Void
 49 |
 50 | ||| The coproduct on APIs.
 51 | public export
 52 | (+) : (c1, c2 : API) -> API
 53 | (+) c1 c2 = (!>) (c1.message + c2.message) (choice c1.response c2.response)
 54 |
 55 | ||| The product of APIs, it uses a product on the messages and a co-product on the responses.
 56 | public export
 57 | (*) : (c1, c2 : API) -> API
 58 | (*) c1 c2 = (x : c1.message * c2.message) !> c1.response x.π1 + c2.response x.π2
 59 |
 60 | ||| The tensor on APIs, a product on both message and responses.
 61 | public export
 62 | (//) : (c1, c2 : API) -> API
 63 | (//) c1 c2 = (x : c1.message * c2.message) !> c1.response x.π1 * c2.response x.π2
 64 |
 65 | ||| Extension of a container as a functor.
 66 | public export
 67 | record Ex (c : API) (ty : Type) where
 68 |   constructor MkEx
 69 |
 70 |   ||| Request
 71 |   req : c.message
 72 |
 73 |   ||| Continuation
 74 |   cont : c.response req -> ty
 75 |
 76 | ||| Substitution monoidal product, aka composition of APIs.
 77 | public export
 78 | (&>) : (c1, c2 : API) -> API
 79 | (&>) c1 c2 = (x : Ex c1 c2.message)
 80 |              !> Σ (c1.response x.req) (c2.response . x.cont)
 81 |
 82 | ||| Continuation monoidal product.
 83 | public export
 84 | (#>) : (c1, c2 : API) -> API
 85 | (#>) c1 c2 = (x : Ex c1 c2.message)
 86 |              !> ((y : c1.response x.req) -> c2.response (x.cont y))
 87 |
 88 | ||| Ex is a functor.
 89 | export
 90 | (c : API) => Functor (Ex c) where
 91 |   map f x = (MkEx x.req (f . x.cont))
 92 |
 93 | ||| Lifting a functor on types into a functor on APIs
 94 | public export
 95 | Lift : (f : Type -> Type) -> API -> API
 96 | Lift f c = (x : c.message) !> f (c.response x)
 97 |
 98 | public export
 99 | ($-) : (f : Type -> Type) -> API -> API
100 | ($-) = Lift
101 |
102 | public export
103 | Send : API -> API
104 | Send c = c.message :- Unit
105 |