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 instantiations of the following two function templates (in hashtblref.sats) for the type we are using:

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.

Functional Map based on AVL Tree

Files to use

staload FM =
"libats/SATS/funmap_avltree.sats"
staload _(*FM*) =
"libats/DATS/funmap_avltree.dats"

Function template to instantiate

fun{key:t0p}
compare_key_key (x1: key, x2: key):<> int

Note that the instantiations of the function template for common types such as int have been provided in funmap_avltree.dats. The code is shown below.

implement
{key}
compare_key_key
  (k1, k2) = gcompare_val_val<key> (k1, k2)
// end of [compare_key_key]