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:t@ype} 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) = eq_int_int (x, y)
implement eq_elt_elt<double> (x, y) = eq_double_double (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 eq_int_int and eq_double_double (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:t@ype}
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 based on a call 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 present in the same 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:t@ype}
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. Both listeq and listeqf have advantages over the other. The former is a first-order function while the latter is a higher-order one, and thus it is likely for the former to be compiled into more efficient object code. However, the latter often seems more convenient for use in practice.

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