Constraint-Solving during Typechecking

Typechecking in ATS involves generating and solving constraints. As an example, the code below implements the well-known factorial function:

fun fact{n:nat} ( x: int(n) ) : [r:nat] int r = if x > 0 then x * fact(x-1) else 1 // end of [fact]

In this implementation, the function fact is assigned the following type:

{n:nat} int(n) -> [r:nat] int(r)

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:

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*r1). 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).