Re: [Caml-list] Problem with universal functions in a module

[Leo White <lpw25@cam.ac.uk>]

> I don't see how there can be much added complexity involved. The
> higher-rank polymorphism is already allowed in records and objects so
> the type system knows how to deal with them. At least when they are
> annotated. I wouldn't need ocaml to infere those types.

It is possible that higher-rank types would not add too much complexity
to OCaml.

However, there is an important difference between that and the
higher-rank polymorphism provided by records and objects: whether to
instantiate a type or not must be inferred. For example, compare this
example using polymorphic methods:

    let f (x : < m: 'a. 'a -> 'a >) =
      let poly =
        if true then x
        else object method m : 'a. 'a -> 'a = id end
      in
      let mono =
        if true then x#m
        else (fun x -> x + 1)
      in
        (poly, mono)

with this example using proper higher-rank types:

    let f (x : 'a. 'a -> 'a) =
      let poly =
        if true then x
        else id
      in
      let mono =
        if true then x
        else (fun x -> x + 1)
      in
        (poly, mono)

Using objects with polymorphic methods we can trivially see that the
first use of `x` is not instantiated whilst the second use of `x` is
instantiated because the first uses the object itself whilst the second
uses the method `m`.

With higher-rank polymorphism, we must infer this information. I don't
think this can be done in a principal way, without adding complexity to
the type langauge (see MLF), so there would need to be some additional
type annotations.

Regards,

Leo