Re: polymorphic recursion

[Xavier Leroy <leroy@welcome.disi.unige.it>]

[On the scope and binding location of type variables in type constraints:]

> This has already been solved in the SML standard and even if it is not 
> necessarily easy to understand when formalized, this is quite intuitive :

[SML'90 rule snipped]

Actually, SML'97 adds explicit scoping of type variables if desired.
The syntax is something like

        let 'a val x = ...

(This is from memory, I don't have the '97 Definition here.)
Although those declarations are optional and the old rule is used
if they are omitted, it shows that maybe the old rule is a little too
subtle to be understood by all.

IT is amusing to notice that SML, Caml and Haskell implement three
different semantics for type variables in constraints:
  - SML: bind at "let" enclosing all mentions of the variable
  - Caml: bind at nearest "struct ... let x = ... end";
  - Haskell: bind immediately in type expression itself (I think).

This is one of those little dark spots in ML-style languages that I
hope will be cleaned some day by drastic simplifications (as the
problem with polymorphic refs was drastically simplified by the value
restriction).  (Argumented) suggestions are welcome.

- Xavier Leroy