Re: [Caml-list] "Type constructor b would escape its scope"

[Leo White <leo@lpw25.net>]

> So here's a question which has been nagging me for a while: is there any occasion where
> one may prefer to use the `(type a)` or the `'a.` forms over the `type a.` (apart for
> syntactical reasons)? If there is I'd be really interested in seeing an example, for I
> can't come up with one (especially for `(type a)`). If there aren't, what are the
> obstacles to turn the `(type a)` syntax into a synonymous to the `type a.` syntax? (I'm
> guessing that the `'a.` variant would be significantly harder).

If you don't need the polymorphism provided by `type a.` then `(type a)`
might be slightly preferable because you don't need to fully describe
the type of the value.

For example, if you are writing a function with type `'a -> 'a` then for
the first form you must write:

    let f : type a. a -> a = fun x -> x

you cannot write:

    let f : type a. a -> _ = fun x -> x

whereas with the second form you could write:

    let f (type a) (x : a) = x

which infers the return type as `a` without the need to annotate it.

This also illustrates what is difficult about reliably turning `(type
a)` into `type a. ...`. For the second form you must work out the entire
type involving `a`. Since `type a. ...` is for polymorphic recursion,
you must do this before you properly type-check the body of the
function.

For a simple case, like:

  let f (x : a) : a = x

it is not too bad as you can examine the argument pattern and constraint
to get the full type, but as the patterns and expressions get more
complicated this becomes more difficult, and at some point you are
forced to draw the line and give up. Finding a sensible place to draw
this line, without making inference unpredictable and confusing to
users, is difficult.

Regards,

Leo