Polymorphic Functions

A polymorphic function is rather similar to a function template. However, the former is a first-class value in ATS while the latter is not. As an example, the following defined function swap_boxed is polymorphic:

fun swap_boxed{a,b:type} (xy: (a, b)): (b, a) = (xy.1, xy.0)

The type variables a and b are often referred as static arguments while xy is a dynamic argument. For example, the following code makes use of the polymorphic function swap_boxed:

val AB = (box("A"), box("B")) val BA1 = swap_boxed{boxstr,boxstr} (AB) val BA2 = swap_boxed (AB) // omitting type arguments may be fine

where the type boxstr is an explicitly boxed version of string that is defined as boxed(string). Internally, there is really no difference between string and boxed(string). If swap_boxed is called on a pair of the type (T1, T2) for some types T1 and T2, both T1 and T2 are required to be boxed. Otherwise, a type-error is reported. For example, calling swap_boxed on (0, 1) yields a type-error as the type int is not boxed. One may be attempted to form a boxed integer like box(0), but doing so leads to a type-error as there is no assumption made about the size of an integer value of the type int in ATS.

When calling a polymorphic function, we often omit passing static arguments explicitly and expect them to be synthesized by the compiler. However, there are also occasions, which are not uncommon, where static arguments need to be supplied explicitly as either they cannot be successfully synthesized or what is synthesized is not exactly what is expected by the programmer.

It is also possible to pass static arguments sequentially as is shown in the following style of implementation of a polymorphic function:

// fun swap2_boxed{a:type}{b:type} (xy: (a, b)): (b, a) = (xy.1, xy.0) // val AB = (box("A"), box("B")) val BA1 = swap2_boxed (AB) // both static arguments to be synthesized val BA2 = swap2_boxed{...} (AB) // both static arguments to be synthesized val BA3 = swap2_boxed{..}{boxstr} (AB) // 1st static argument to be synthesized val BA4 = swap2_boxed{boxstr}{..} (AB) // 2nd static argument to be synthesized val BA5 = swap2_boxed{..}{..} (AB) // both static arguments to be synthesized val BA6 = swap2_boxed{boxstr}{boxstr} (AB) // both static arguments are provided //

The special syntax {..} indicates to the typechecker that the static argument (or arguments) involved in the current application should be synthesized while the special syntax {...} means that the rest of static arguments should all be synthesized.

I have seen two kinds of errors involving polymorphic functions that are extremely common in practice.

Given the potential confusion, why do we need both function templates and polymorphic functions? At this stage, it is certainly plausible that we program only with function templates and make no use of polymorphic functions. However, polymorphic functions simply become indispensible in the presence dependent types. There will actually be numerous occasions where we encounter polymorphic function templates, that is, templates for polymorphic functions.