The integer addition function can be assigned the following (dependent) type in ATS to indicate that it returns the sum of its two integer arguments:

This type gives a full specification of integer addition as the only (terminating) function that can be given the type is the integer addition function. However, the factorial function, which yields the product of the first n positive integers when applied to a natural number n, cannot be given the following type: as fact, which refers to the factorial function, does not exist in the statics of ATS. Evidently, a highly interesting and relevant question is whether a type can be formed in ATS that fully captures the functional relation specified by fact? The answer is affirmative. We can not only construct such a type but also assign it to a (terminating) function implemented in ATS.Let us recall that the factorial function can be defined by the following two equations:

Naturally, these equations can be encoded by the constructors associated with the dataprop FACT declared as follows:dataprop FACT(int, int) = | FACTbas(0, 1) | {n:nat}{r1,r:int} FACTind(n, r) of (FACT(n-1, r1), MUL(n, r1, r)) // end of [FACT]

// fun ifact {n:nat} .<n>. ( n: int(n) ) :<> [r:int] (FACT(n, r) | int r) = ( // if n = 0 then (FACTbas() | 1) else let val (pf1 | r1) = ifact (n-1) // pf1: FACT(n-1, r1) val (pfmul | r) = imul2 (n, r1) // pfmul: FACT(n, r1, r) in (FACTind(pf1, pfmul) | r) end // end of [else] // ) (* end of [ifact] *) //

Please find the entirety of the above presented code plus some testing code on-line.