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:
Note that for any given natural number n and integer r,
FACT(n, r)
can be assigned to a proof if and only if
fact(n) = r. Therefore,
the following type
can only be assigned to a function that, if applied to a natural number n,
returns a proof and an integer such that the proof attests to the integer
being equal to
fact(n). For instance, the following defined
function
ifact is assigned this type:
After proof erasure,
ifact precisely implements the factorial function.
Please find the entirety of the above presented code plus some testing code
on-line.