Introduction to Programming in ATS:
Prev	Chapter 5. Parametric Polymorphism	Next

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.

The first kind is depicted in the following example:
```
fun swap_boxed{a,b:t@ype} (xy: (a, b)): (b, a) = (xy.1, xy.0)
```
Notice that the sort for type variables a and b is t@ype (instead of type). While this example can pass typechecking, its compilation results in a compile-time error that may seem mysterious to many programmers. The simple reason for this error is that the compiler cannot figure out the size of a and b when trying to generate code in C as the sort t@ype is for types of unspecified size.
The second kind is depicted in the following example:
```
fun{a,b:type} swap_boxed (xy: (a, b)): (b, a) = (xy.1, xy.0)
```
Strictly speaking, there is really no error in this case. If defined as such, swap_boxed is a function template instead of a polymorphic function. However, such a function template is severely restricted as it cannot be instantiated with types that are not boxed. While this could be intended, it is very unlikely.

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.