## MLton 20241230

# 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.