FYI.
There are some convenience functions in prelude/SATS/checkast.sats
for performing dynamic checking:
http://www.ats-lang.org/LIBRARY/prelude/checkast.html
Say we have the following function [fact]:
fun fact
{n:nat}(x: int n): int
if x > 0 then x * fact(x-1) else 1
The type assigned to [fact] indicates that it can only be applied to a
non-negative integer.
Suppose that the integer input comes from the keyboard. Then dynamic
checking needs to
be performed on the integer to ensure that it is non-negative:
implement
main0 (argc, argv) = let
//
val n =
(
if argc >= 2 then g0string2int(argv[1]) else 10
) : int
//
val n = ckastloc_gintGte (n, 0) // dynamic checking
//
in
println! (“fact (”, n, ") = ", fact(n))
end // end of [main0]
The type of ckastloc_gintGte is: {i:int} (int, int(i)) -> intGte(i).
Given two integers n and i, ckastloc_gintGte(n, i) returns n if n >= i;
otherwise, a run-time
error is issued.
Essentially, the line ‘val n = ckastloc_gintGte (n, 0)’ is equivalent to
the following two lines:
val n = g1ofg0 (n) // assigning [n] a dependent type
val () = assertloc (n > 0) // performing dynamic checking
When programming in ATS, it is often a good idea to first use dynamic
checking
(instead of types and theorem-proving) to get a piece of code to pass
typechecking.
This is especially true for beginners.
Happy programming!