Specific Template Implementation

Implementing an interface for a function template specifically means to give an implementation for a fixed instance of the template. For instance, the following interface is for a function template of the name eq_elt_elt:

fun{a:t0p} eq_elt_elt (x: a, y: a): bool // a generic equality

There is no meaningful generic implementation for eq_elt_elt as equality test for values of a type T depends on T. Two specific template implementations are given as follows for the instances eq_elt_elt<int> and eq_elt_elt<double>:

implement eq_elt_elt<int> (x, y) = g0int_eq (x, y) implement eq_elt_elt<double> (x, y) = g0float_eq (x, y)

where eq_int_int and eq_double_double are equality functions for values of the type int and double, respectively. It is also possible to give the implementations as follows:

implement eq_elt_elt<int> (x, y) = (x = y) implement eq_elt_elt<double> (x, y) = (x = y)

This is allowed as the symbol = is already overloaded with g0int_eq and g0float_eq (in addition to many other functions).

Let us now see a typical use of specific template implementation. The following defined function template listeq implements an equality function on lists:

fun{ a:t0p } listeq ( xs: list0 a , ys: list0 a ) : bool = ( case+ (xs, ys) of | (list0_cons (x, xs), list0_cons (y, ys)) => if eq_elt_elt<a> (x, y) then listeq (xs, ys) else false | (list0_nil (), list0_nil ()) => true | (_, _) => false ) (* end of [listeq] *)

Given two lists xs and ys, listeq returns true if and only if xs and ys are of the same length and each element in xs equals the corresponding one in ys (according to eq_elt_elt). Given a type T, it is clear that the instance eq_elt_elt<T> is needed if listeq is called on two lists of the type list0(T). In other words, a specific implementation for eq_elt_elt<T> should be given if a call to listeq is to be made on two lists of the type list0(T). Note that the implementation for an instance of a function template is required to be accessible from the file where the instance is called.

As a comparison, the following defined function template listeqf also implements equality test on two given lists:

fun{ a:t0p } listeqf ( xs: list0 a , ys: list0 a , eq: (a, a) -> bool ) : bool = ( case+ (xs, ys) of | (list0_cons (x, xs), list0_cons (y, ys)) => if eq (x, y) then listeqf (xs, ys, eq) else false | (list0_nil (), list0_nil ()) => true | (_, _) => false ) (* end of [listeqf] *)

In this case, listeqf takes an additional argument eq that tests whether two list elements are equal. As listeq is a first-order function while listeqf is a higher-order one, it is likely for the former to be compiled into more efficient object code. I would like to point out that the library of ATS makes pervasive use of specifically implemented templates.

Please find the code presented in this section plus some additional testing code available on-line.