Overview
The APIs exposed by the servers accept parameters that are each
implicitly of a given type. Because
HTTP only exposes an interface that only allows parameters to be
arbitrary character strings, it's necessary to give
interpretive typing rules. That is,
the rules state that a given string s
is of type t iff
s
can be interpreted as a value of
type t according to the given set of
rules for t.
As an example, a string s
can be interpreted as a value of type integer
iff the contents of the string match the pattern
0 | [1-9][0-9]*.
The purpose of giving typing rules in this style is so that APIs
can be defined in terms of the types of the parameters, and a programmer
reading the API definition need only look up the definitions of the types
to know how to correctly format string values for the API. Additionally,
developers may be speaking to the server from any number of different
programming languages. The rules are given in terms of an extremely
simple pure-functional language and so are easily mapped
to code written in more or less any modern programming language.
Typing Rules
Rules are specified in terms of combinations of
functions
over
string,
character,
integer, and
boolean types.
The syntax s : t
means that s is of
type t. The syntax
f : t → u states
that f is a function
that takes a value of type t
and returns a value of type u.
The syntax f : (t,u) → v
states that f is
a function that takes two arguments, the first of type
t and the second of
type u and returns
a value of type v.
The syntax f(x) is
the application of a unary function
f to a value
x. The syntax
f(x,y) is the application
of a two-argument function f
to values x and
y.
The syntax ∀i. p(i)
introduces a new universally-quantified variable
i and states that
the function p
evaluates to true
for i. In other words,
"for every possible i,
p holds for
i".
The syntax ∃i. p(i)
introduces a new existentially-quantified variable
i and states that
the function p
evaluates to true
for i. In other words,
"there exists some i,
such that p holds for
i".
The expression x ∧ y
evaluates to true
if both x and
y evaluate to
true. If
x evaluates to
false, then
y is not evaluated
and the whole expression evaluates to
false. This is the
same short-circuit logic
seen in the AND
operators of most programming languages. The
∧ operator is left-associative,
so x ∧ y ∧ z = (x ∧ y) ∧ z.
The expression x ∨ y
evaluates to true
if either of x or
y evaluates to
true. The
∧ operator is left-associative,
so x ∨ y ∨ z = (x ∨ y) ∨ z.
Predefined Types
The predefined boolean
type has two values: true
and false.
The predefined integer
type represents integer values in the exclusive range
(-∞, ∞).
The predefined character
type represents a Unicode codepoint. Specific character
values are given in type rules by the syntax
U+NNNN,
where N represents a hexadecimal
digit. For example, U+03BB
corresponds to the lowercase lambda symbol
λ.
Characters are placed into categories according to the
Unicode standard, For example, the character
U+0037, corresponding
to the digit 7 is in the DECIMAL_DIGIT_NUMBER
category.
The predefined list[t]
type represents a bounded list of values of type
t.
The predefined string
is a synonym for the type
list[character].