TDL
TDL is a language for describing data types. These data types can be converted into data types in other languages, along with operations such as equality checks and serialization.
Syntax
Modules
Types
The type system of TDL features primitive types, product types, sum types, parameterized types, and higher-kinded types.
Primitive Types
The following primitive types exist:
| Type | Kind | Summary |
|---|---|---|
bool |
* |
Boolean |
i32 |
* |
32-bit signed integer, range \(\left[-2^{31}, 2^{31} - 1\right]\) |
f64 |
* |
IEEE 754 double precision floating point number |
text |
* |
Unicode text |
array |
* -> * |
Array of anything |
bytes |
* |
Packed array of octets |
Product Types
Sum Types
Due to code generation limitations, non-empty sum types may not be part of other types; they must appear directly as top-level definitions.
Kind Checking
TDL checks that types are well-kinded. For example, one cannot
apply the array type to two type arguments, as in
array i32 i32. The kind checker verifies this. The
kind checker applies the following inference rules:
$$
\begin{array}{ c l }
\irule{\tau : \kappa \in \Gamma}{\G \tau : \kappa} & \mathtt{Var} \\ \\
\irule{\G \tau : \kappa \rightarrow \iota \quad \G \sigma : \kappa}{\G \tau \sigma : \iota} & \mathtt{App} \\ \\
\irule{\G \overline{\tau_i : \Seri \vphantom{l}}}{\G \Rec{\overline{l_i : \tau_i}} : \Seri} & \mathtt{Product} \\ \\
\irule{\G \overline{\tau_i : \Seri \vphantom{l}}}{\G \Sum{\overline{l_i : \tau_i}} : \Seri} & \mathtt{Sum} \\ \\
\end{array}
$$
Services
A service is a method that can be called over a network. TDL generates functions to call services and functions to define services. An example of a service declaration follows:
service GetUser : UserID -> maybe User;
A service has a request type and a response type. The request type
appears on the left-hand side of the arrow, whereas the response type
appears on the right-hand side of the arrow. Both types must be of
kind *.