Re: polymorphic recursion

[Peter Thiemann <pjt@cs.nott.ac.uk>]

>>>>> "Pierre" == Pierre Weis <Pierre.Weis@inria.fr> writes:

    Pierre> I suggest the following simple rules:

    Pierre> (1) type expressions appearing in type constraints are supposed to be
    Pierre> type schemes, implicitely quantified as usual. Scope of type variables
    Pierre> is simply delimited by the parens surrounding the type constraint.

    Pierre> (2) a type constraint (e : sigma) is mandatory. It means that sigma IS
    Pierre> a valid type scheme for e, and indeed sigma is the type scheme
    Pierre> associated to e by the compiler. (This implies that sigma is an
    Pierre> instance of the most general type scheme of e.)

This suggestion is quite close to what Haskell imposes, as far as I
know: if there is a top-level type signature for an identifier f, then
it is taken as a type scheme (implicitly all-quantifying all type
variables) and *all* occurrence of f (including recursive ones) are
type-checked using this signature as assumption.
Furthermore, the inferred type scheme for the body of f must be more
general than its type signature prescribes.

This corresponds to the typing rule

A, f:sigma |- e : sigma'
--------------------------- sigma is a generic instance of sigma'
A |- fix f:sigma. e : sigma

Here is a drawback of your proposal that the Haskell folks are
currently addressing in a revision of the standard:
you cannot always write a type signature for a nested function.
Suppose

let (f : 'a * 'b -> 'b) =
  fun (x, y) ->
    let (g : unit -> 'b) =
      fun () -> y
    in g ()

[this would not type check]
In this case, g really has *type* unit -> 'b without 'b being
all-quantified. Of course, you could write something like:

let (f : 'a * 'b -> 'b) =
  fun (x, (y : '_b)) ->
    let (g : unit -> '_b) =
      fun () -> y
    in g ()

but that would not be nice.
If I recall correctly, the current Haskell proposal says that
variables in the outermost type signature are bound in the body of the 
corresponding definition.
That's not nice, either.

An alternative that I could imagine is to include explicit binders for 
the type variables, i.e., big Lambdas, to indicate their scope
precisely in the rare cases where it is necessary. It could be
regarded an error to mix explicitly bound and implicitly bound type
variables, as this might give rise to misunderstandings.

Having a unified treatment for these things would really make life
easier.

-Peter