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 <:StandardML:Standard ML> does have
polymorphic functions, it does not support first-class polymorphism.

For example, the following declares and uses the polymorphic function
`id`.
[source,sml]
----
val id = fn x => x
val _ = id 13
val _ = id "foo"
----

If SML supported first-class polymorphism, we could write the
following.
[source,sml]
----
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.
[source,sml]
----
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
[source,sml]
----
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?
[source,sml]
----
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
<:TypeVariableScope:scoping the type variables>.
[source,sml]
----
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.