A Tutorial on Programming Features in ATS:
<<< PreviousNext >>>

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: 

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

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: 

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

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. 

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 ()
// end of [lstlst]

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 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

<<< PreviousHomeNext >>>
Advanced Tutorial TopicsUpStack Allocation at Run-Time