Introduction to Programming in ATS:
<<< Previous	Introduction to Dependent Types	Next >>>

Constraint-Solving during Typechecking

Typechecking in ATS involves generating and solving constraints. As an example, the code below gives an implementation of the 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:

For each natural number n, n > 0 implies n - 1 >= 0
For each natural number n and each natural number r₁, n > 0 implies n * r₁ >= 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₁). 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 coven the issue of explicit proof construction in an elaborated manner elsewhere.

As a more interesting example, the following code implements MacCarthy's famous 91-function:

fun f91 {i:int} (x: int i)
  : [j:int | (i < 101 && j==91) || (i >= 101 && j==i-10)] int (j) =
  if x >= 101 then x-10 else f91 (f91 (x+11))
// end of [f91]

The type assigned to f91 clearly indicates that the function always returns 91 if its argument is less than 101 or it returns the difference between its argument and 10. The constraints generated during typechecking in this example are all linear and can be readily solved by the the constraint-solver employed by the typechecker of ATS.

Currently, the constraint-solver implemented for ATS/Anairiats makes use of machine-level arithmetic (in contrast to the standard arithmetic of infinite precision). This is done primarily for the sake of efficiency. In the presence of machine-level arithmetic overflow during constraint-solving, results returned by the constraint-solver are likely to be incorrect. While such cases can be readily constructed, their appearances in practice seem rare.

<<< Previous	Home	Next >>>
Introduction to Dependent Types	Up	Example: String Processing