template

#INV

INV (for invariant) is essentially marker for typechecking [1]. For instance, say you have a function foo declared as follows:

fun{a:t@ype} foo (xs: list0 (a)): void

Assume that mylst is of the type list0 (T) for some T. When typechecking foo(mylst), the typechecker will expand the expression as follows by picking a placeholder T1:

foo<T1>(mylst)

where T <= T1 is assumed, so that mylst can contain any subtype--in the covariant sense--of T1 [2]. Say that foo2 is declared as follows:

fun{a:t@ype} foo2 (xs: list0 (INV(a))): void

When foo2(mylst) is typechecked, the typechecker simply expands the expression to the following one:

foo2<T>(mylst)

preventing types other than precisely T to be a part of mylst.

Examples of using templates

Hashmap (mutable)

ATS is shipped with library code for mutable hash map. libats/ML/SATS/hashtblref.sats contains declaration for related types and functions. The related template code resides in the following files:

libats/DATS/hashfun.dats
libats/DATS/linmap_list.dats
libats/DATS/hashtbl_chain.dats
libats/ML/DATS/hashtblref.dats

To use the hash map in a dats file, we need to put the following into the dats file:

staload HT = "libats/ML/SATS/hashtblref.sats"

staload _(*anon*) = "libats/DATS/hashfun.dats"
staload _(*anon*) = "libats/DATS/linmap_list.dats"
staload _(*anon*) = "libats/DATS/hashtbl_chain.dats"
staload _(*anon*) = "libats/ML/DATS/hashtblref.dats"

Also we need to provide implementation for the following two function templates, which are declared in hashtblref.sats:

fun{
key:t0p
} hash_key (x: key):<> ulint
//
fun{
key:t0p
} equal_key_key (x1: key, x2: key):<> bool

Note that the instantiations of these two function templates for common types such as int or string have been provided in hashtblref.dats.