In ATS, when a dynamic constant (usually a function)
is declared, its type must be given as well. For instance:
extern
fun{a:t@ype}
list_append{m,n:nat} (list(a, m), list(a, n)): list(a, m+n)
Sometimes, it can be very convenient if we have a way to
refer to the type assigned to a dynamic constant. For instance,
list_append can be implemented as follows:
implement
{a} // tmparg
list_append =
append where
{
//
fun append
: $d2ctype(list_append) =
lam(xs, ys) =>
case+ xs of list_nil() => ys | list_cons(x, xs) => list_cons(x, append(
xs, ys))
//
} // end of [list_append]
where the expression $d2ctype(list_append) refers to the type assigned
to list_append.
This is now supported in ATS2-0.2.2 (just released).
Of course, list_append can also be implemented as follows:
implement
{a} // tmparg
list_append(xs, ys) =
case+ xs of
| list_nil() => ys
| list_cons(x, xs) => list_cons(x, list_append(xs, ys))
// end of [list_append]
This implementation makes use of recursive template instantiation, which is
not a preferred
style as it can cause complications during the compilation of template
instantiation.