FirstClassPolymorphism

First-class polymorphism is the ability to treat polymorphic functions just like other values: pass them as arguments, store them in data structures, etc. Although Standard ML does have polymorphic functions, it does not support first-class polymorphism.

For example, the following declares and uses the polymorphic function id.

val id = fn x => x
val _ = id 13
val _ = id "foo"

If SML supported first-class polymorphism, we could write the following.

fun useId id = (id 13; id "foo")

However, this does not type check. MLton reports the following error.

Error: z.sml 1.24-1.31.
  Function applied to incorrect argument.
    expects: [int]
    but got: [string]
    in: id "foo"

The error message arises because MLton infers from id 13 that id accepts an integer argument, but that id "foo" is passing a string.

Using explicit types sheds some light on the problem.

fun useId (id: 'a -> 'a) = (id 13; id "foo")

On this, MLton reports the following errors.

Error: z.sml 1.29-1.33.
  Function applied to incorrect argument.
    expects: ['a]
    but got: [int]
    in: id 13
Error: z.sml 1.36-1.43.
  Function applied to incorrect argument.
    expects: ['a]
    but got: [string]
    in: id "foo"

The errors arise because the argument id is not polymorphic; rather, it is monomorphic, with type 'a -> 'a. It is perfectly valid to apply id to a value of type 'a, as in the following

fun useId (id: 'a -> 'a, x: 'a) = id x  (* type correct *)

So, what is the difference between the type specification on id in the following two declarations?

val id: 'a -> 'a = fn x => x
fun useId (id: 'a -> 'a) = (id 13; id "foo")

While the type specifications on id look identical, they mean different things. The difference can be made clearer by explicitly scoping the type variables.

val 'a id: 'a -> 'a = fn x => x
fun 'a useId (id: 'a -> 'a) = (id 13; id "foo")  (* type error *)

In val 'a id, the type variable scoping means that for any 'a, id has type 'a -> 'a. Hence, id can be applied to arguments of type int, real, etc. Similarly, in fun 'a useId, the scoping means that useId is a polymorphic function that for any 'a takes a function of type 'a -> 'a and does something. Thus, useId could be applied to a function of type int -> int, real -> real, etc.

One could imagine an extension of SML that allowed scoping of type variables at places other than fun or val declarations, as in the following.

fun useId (id: ('a).'a -> 'a) = (id 13; id "foo")  (* not SML *)

Such an extension would need to be thought through very carefully, as it could cause significant complications with TypeInference, possible even undecidability.