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:

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)

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] *)

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] *)

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