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)

val AB = ("A", "B")
val BA1 = swap_boxed {string,string} (AB) // [string] is boxed
val BA2 = swap_boxed (AB) // this is fine, too

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.

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 = ("A", "B")
val BA1 = swap2_boxed {string} {string} (AB)
val BA2 = swap2_boxed (AB) // this is fine, too
val BA3 = swap2_boxed {..} {string} (AB) // 1st static argument to be synthesized
val BA4 = swap2_boxed {string} {..} (AB) // 2nd static argument to be synthesized
val BA5 = swap2_boxed {..} {..} (AB) // both arguments to be synthesized
val BA6 = swap2_boxed {...} (AB) // every static argument to 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 an 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 likely not.