Re: polymorphic recursion

[Pierre Weis <Pierre.Weis@inria.fr>]

> This suggestion is quite close to what Haskell imposes
[...]

> Furthermore, the inferred type scheme for the body of f must be more
> general than its type signature prescribes.

Yes, this is implicit in the rule I proposed.

[...]

> 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.

That's why I considered extending type constraints to not quantified
type variables.

[...]

> 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.

I agree with you that this is not that nice, although perfectly
unambiguous. On the other hand, the Haskell proposal does not solve
the fundamental problem: type constraints are still puzzling, since
the confusing between quantified type variables and not quantified
type variables still remains.

This confusion is avoided if we extend type constraints to '_ type
variables.  Note also that the sharing type constraint you pointed out
is complex and hardly ever necessary in practice. (Anyway you
perfectly succeeded in expressing it in the framework of my proposal.)

> 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.

In my mind, explicit binders for type variables would be a major
change in the language, and may not be worth the
modification. Remember that we mainly want to get rid of meaningless
(or puzzling) type annotations and get an easy way to typecheck
polymorphic recursive functions.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/