Why Apilog?¶
Focused on API Testing¶
A lot of communication between software services and applications follow simple request-response RPC protocols. A common example is JSON over HTTP which has almost become the lingua franca of RPC communication. Apilog is language for concise specification, documentation and testing of RPC interfaces, or APIs (as they are often called).
Based on Logic¶
In contrast to API description formats like OpenAPI, Apilog is a typed logic programming language. This has some advantages, like the possibility to sprinkle (properly scoped and typed) quantified variables over API descriptions to express relationships between parameters. Or to express pre- and post-conditions of API operations in the form of logical formulas. It also lets one write non-deterministic test data generators for API requests. Documentation annotations can be attached to formulas, which preserves some of the aspects of an OpenAPI-like description. Here is an example of an API endpoint definition in this language:
api create_user :=
summary "Creates a new user" ?
description U "The name of the new user" ?
{post /users _ U}(R\ status 200 R, user U; status 409 R).
The right hand side of this definition is a logical formula. Like in
Prolog, (unbound) capitalized
identifiers are implicitly quantified. The formula should be read as follows:
For all strings U, after sending an HTTP request with method POST, path
/users, and body U, one should receive response R with status 200 OK,
and there should exist a new user named U, or R has status 409
Conflict, and there is no new user. Type inference takes care of figuring out
the types of variables, and quoting variables where necessary (e.g. for
arguments to documentation combinators). In this example the body of the
request is simply the username, for the sake of simplicity.
So, we have seen that variables are capitalized but constants are not; a notation that comes from Prolog. Some other fundamental aspects are also borrowed from Prolog, but otherwise Apilog is more closely related to a more recent family of languages, developed from a proof-theoretical view of logic programming. In particular, Apilog is influenced by Lambda Prolog, Lolli, LolliMon and Bedwyr.
With its foundation in logic, we think Apilog could unify some tendencies and combine some things that one may want when working with APIs:
- Property-based testing
- APIs as type signatures (think of, e.g., Haskell's Servant library)
- Generation of client and server bindings for implementation languages
- Generation of documentation
Modal¶
Apilog has a language construct to express what should hold true after an
action. This construct takes an action expression between curly braces,
followed by a predicate on the result value of the action. For example, to
define an HTTP API in which all GET requests to path /foo should yield a
response with status 200, one can write:
api all_ok := {get /foo _}(R\ status 200 R).
Here, the expression get /foo _ between curly braces is an action expression.
The underscore means we have the headers of the request unspecified. To the
right is a function (R\ is syntax for lambda binding) from the action result
R to the formula status 200 R, expressing that the response status must be
200.
This language construct is inspired by modal logic, in particular lax logic, but also program logics such as dynamic logic.
Linear¶
Apilog uses (intuitionistic) linear logic to express state changes by interpreting formulas as resources. To illustrate this, let us expand on the original example of creating users. First, to write such API definitions we must first have declared a new kind of resource formula to represent users in our system:
resource user : string -> prop.
The string argument is the user name and prop is the type of logical
formulas. Next, let us re-use the create_user definition we made earlier, and
also add an endpoint for deleting users:
api create_user := {post /users _ U}(R\ status 200 R, user U; status 409 R).
api delete_user := user U -o {/delete /users/U _ _}(_\ one).
api user_api :=
create_user &
delete_user.
If you are not familiar with linear logic, you can think of the symbol -o as
kind of implication arrow, , as conjuction and ; as disjunction. The
constant one is a formula that represents an empty set of resources, and the
formula user U represents a user resource with name U.
To understand the state changes specified in the example, pay attention to
where the formula user U occurs. In create_user it occurs in the predicate
that must hold after the action. This means it is a post-condition, and that
the resource may exist after the action in the formula has been performed (if
the status is 200).
In delete_user, on the other hand, user U occurs in the antecedent (to the
left) of the implication arrow. This means it is a pre-condition and that a
resource user U must exist in order for post-condition to hold after making
the delete action. Moreover, due to how linear implication works (it consumes
resources), and because the user resource does not re-appear in the
post-condition, the user resource must no longer exist after making the action.
Parallel¶
Apilog executes tests in parallel in order to find a wider class of bugs and to achieve higher test throughput. The parallelism is deterministic in the sense that parallel tests generated by Apilog must be possible to run in parallel without interference, simply as a consequence of the API specification (and the underlying logic). Of course, the goal is to try to uncover cases where that promise does not hold, i.e. a bug in the API specification or in the system under test.
The Apilog interpreter implements parallel testing by keeping track of a single set of assumptions about the state, across concurrent processes, managing ownership and sharing automatically. This system is made possible largely thanks to the linear logic component, and in that respect the system has some similarity to e.g. the race-free concurrency of Rust. In the future we would like to go further in this direction and add uniqueness logic, to get finer-grained sharing of resources.