Typechecking in ATS involves generating and solving constraints.
As an example, the code below implements the well-known factorial
function:
In this implementation, the function
fact is assigned the
following type:
which means that
fact returns a natural number r when applied
to a natural number n. When the code is typechecked, the following
constraints need to be solved:
For each natural number n, n > 0 implies n - 1 >= 0
For each natural number n and each natural number r1, n > 0 implies n * r1>= 0
For each natural number n, 1 >= 0 holds.
The first constraint is generated due to the call
fact(x-1),
which requires that
x-1 be a natural number. The second
constraint is generated in order to verify that
x * fact(x-1)
is a natural number under the assumption that
fact(x-1) is a
natural number. The third constraint is generated in order to verify that
1 is a natural number. The first and the third constraints can
be readily solved by the constraint solver in ATS, which is based on the
Fourier-Motzkin variable elimination method. However, the second constraint
cannot be handled by the constraint solver as it is nonlinear: The
constraint cannot be turned into a linear integer programming problem due
to the occurrence of the nonlinear term (n*r
1). While nonlinear
constraints cannot be handled automatically by the constraint solver in
ATS, the programmer can verify them by constructing proofs in ATS
explicitly. I will cover the issue of explicit proof construction in an
elaborated manner elsewhere.
By default, the constraint-solver implemented for ATS/Postiats makes use of
the standard arithmetic of infinite precision. For the sake of efficiency,
one may also choose to use machine-level arithmetic for solving integer
constraints. Due to potential arithmetic overflow, results returned by the
constraint-solver that uses machine-level arithmetic can be incorrect (but
I have so far not knowingly encountered such a situation in practice).