# Cast Functions

A cast function in ATS is equivalent to the identify function in terms
of dynamic semantics. A call to such a function is evaluated at
compile-time, and its argument is returned. For instance, we have the
following commonly used cast functions:

Note that the keyword

castfn is for introducing cast functions.

Let us now see a more interesting use of casting functions. The following
declared function interface is intended for concatenating a list of lists:

Assume that we would like to verify that the concatenation of a list of
lists yields a list whose length equals the sum of the lengths of the lists
in the given list of lists. This, for instance, can be done as follows by
introducting a datatype constructor lstlst.

Given a type T and integers I and J, the type

lstlst(T, I, J) is
for a list of lists such that the length of the list is I and each element
in the list is a list of values of the type T and the sum of the lengths of
these elements equals J. The function list_concat is the same as the
function _concat in terms of dynamic semantics, and it can be implemented
as follows:

Given lstlst_of_listlist being implemented as a casting function, the
implementation of list_concat is equivalent to the following one in terms
of dynamic semantics: