Example: A Temptorial Package for Rationals

As I have great difficulty in naming the style of programming I am about to present in this section, I coin a word temptorial (as a shorthand for template-functorial) to refer to this style, which makes essential use of function templates that are implemented generically as well as specifically.

Suppose that we have interfaces for two function templates foo and bar. We give a generic template implementation for bar that makes use of foo but we cannot or do not want to implement foo generically. When an instance of bar is called, certain instances of foo may need to be implemented specifically so as to support the call. Let us now imagine a design where foo and bar are replaced with collections of function templates corresponding to various operations on integers and rationals. This is precisely the idea employed in the design of a temptorial package for rationals.

The following interfaces for function templates are declared in a file named ratfun_tmp.sats, which is available on-line:

fun{a:t@ype} ofint: int -> a
fun{a:t@ype} fprint_int (out: FILEref, x: a): void

fun{a:t@ype} intneg: a -> a
fun{a:t@ype} intadd: (a, a) -> a
fun{a:t@ype} intsub: (a, a) -> a
fun{a:t@ype} intmul: (a, a) -> a
fun{a:t@ype} intdiv: (a, a) -> a
fun{a:t@ype} intmod: (a, a) -> a

fun{a:t@ype} intcmp: (a, a) -> int

(* ^^^^^^ ^^^^^^ *)
//
// the following templates are implemented based on the above ones
//
(* vvvvvv vvvvvv *)

fun{a:t@ype} intgcd: (a, a) -> a

fun{a:t@ype} intlt: (a, a) -> bool
fun{a:t@ype} intlte: (a, a) -> bool
fun{a:t@ype} intgt: (a, a) -> bool
fun{a:t@ype} intgte: (a, a) -> bool
fun{a:t@ype} inteq: (a, a) -> bool
fun{a:t@ype} intneq: (a, a) -> bool

abst@ype rat (a: t@ype) = (a, a)

fun{a:t@ype} rat_make_int_int (p: int, q: int): rat a
fun{a:t@ype} rat_make_numer_denom (p: a, q: a): rat a

fun{a:t@ype} fprint_rat (out: FILEref, x: rat a): void

fun{a:t@ype} rat_numer (x: rat a): a
fun{a:t@ype} rat_denom (x: rat a): a

fun{a:t@ype} ratneg: (rat a) -> rat a
fun{a:t@ype} ratadd: (rat a, rat a) -> rat a
fun{a:t@ype} ratsub: (rat a, rat a) -> rat a
fun{a:t@ype} ratmul: (rat a, rat a) -> rat a
fun{a:t@ype} ratdiv: (rat a, rat a) -> rat a

fun{a:t@ype} ratcmp: (rat a, rat a) -> int

In another file named ratfun_tmp.dats, which is also available on-line, the second half of the above interfaces for function templates are implemented based on the function templates for which the interfaces are declared in the first half. As an example, the function template rat_make_numer_denom is implemented as follows:

implement{a}
rat_make_numer_denom (p, q) = let
  fun make (p: a, q: a): rat a = let
    val r = intgcd (p, q) in (p \intdiv r, q \intdiv r)
  end // end of [make]
in
  if intgtz (q)
    then make (p, q) else make (intneg p, intneg q)
  // end of [if]
end // end of [rat_make_numer_denom]

Note that the backslash symbol (\) temporarily assigns the infix status to the identifier immediately following it. For instance, the syntax p \intdiv r simply stands for the function application intdiv(p, r).

There is some testing code available on-line that demonstrates a typical way to use a temptorial package. For instance, if we want to use a package for rationals where integers are represented as values of the type double, then we can first give the following specific implementations for instances of function templates corresponding to certain integer operations:

staload M = "libc/SATS/math.sats" // for [fmod]

typedef T = double
implement ofint<T> (x) = double_of (x)
implement fprint_int<T> (out, x) = fprintf (out, "%.0f", @(x))

implement intneg<T> (x) = ~x
implement intadd<T> (x, y) = x + y
implement intsub<T> (x, y) = x - y
implement intmul<T> (x, y) = x * y
implement intdiv<T> (x, y) = $M.trunc (x/y) // trunc: truncation
implement intmod<T> (x, y) = $M.fmod (x, y) // modulo operation

implement intcmp<T> (x, y) = compare (x, y)

With these implementations, we can call the corresponding instances of those function templates in ratfun_tmp.sats (e.g., ratadd<double> and ratsub<double>) that have already been implemented generically.