Generic Template Implementation

Interfaces for function templates are mostly similar to those for functions. For example, the following syntax declares an interface in a dynamic file for a function template of the name list0_fold_left:

extern
fun{
a:t0p}{b:t0p
} list0_fold_left
  (xs: list0 b, f: (a, b) -<cloref1> a, init: a): a

If the same interface is declared in a static file, the keyword extern should be dropped. Implementing an interface for a function template is also mostly similar to implementing one for a function. The above interface for list0_fold_left is given an implementation in the following code:

implement{a}{b}
list0_fold_left
  (xs, f, init) = let
//
fun loop
(
  xs: list0 b, res: a
) : a =
(
  case+ xs of
  | list0_nil () => res
  | list0_cons (x, xs) => loop (xs, f (res, x))
) (* end of [loop] *)
//
in
  loop (xs, init)
end // end of [list0_fold_left]

extern
fun
{a,b:t0p}{c:t0p}
app2 (f: (a, b) -<cloref1> c, x: a, y: b): c

implement{a,b}{c} app2 (f, x, y) = f (x, y)

The style of template implementation presented in this section is referred to as generic template implementation. I will later present a different style of template implementation, which is often referred to as specific template implementation.