Casting Functions

A casting 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 casting functions:

castfn int1_of_int (x: int):<> [n:nat] int n
castfn string1_of_string (x: string):<> [n:nat] string n

The keyword castfn is for introducing casting functions.

We now present a typical use of casting functions. The following declared function list_concat is intended for concatenating a list of lists:

fun{a:t@ype} list_concat (xss: List (List a)): List a

Let us say 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.

datatype lstlst (a:t@ype+, int, int) =
  | {m,t:nat} {n:nat}
    lstlst_cons (a, m+1, t+n) of (list (a, n), lstlst (a, m, t))
  | lstlst_nil (a, 0, 0) of ()

fun{a:t@ype} _concat {m,t:nat} .<m>.
  (xss: lstlst (a, m, t)): list (a, t) = case+ xss of
  | lstlst_cons (xs, xss) => list_append (xs, _concat<a> xss)
  | lstlst_nil () => list_nil ()
// end of [_concat]

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:

implement{a} list_concat (xss) =
  _concat<a> (lstlst_of_listlist xss) where {
  castfn lstlst_of_listlist
    {m:nat} .<m>. (xss: list (List a, m))
    :<> [t:nat] lstlst (a, m, t) = case+ xss of
    | list_cons (xs, xss) => lstlst_cons (xs, lstlst_of_listlist xss)
    | list_nil () => lstlst_nil ()
} // end of [list_concat]

Given that 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:

implement{a} list_concat (xss) = _concat (xss) // this one does not typecheck

The code used for illustration is available here.