polymorphic recursion

polymorphic recursion

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 142 bytes --]

Hello list,
I'm having trouble finding information on this; does ocaml support
polymorphic recursion and, if so, what's the syntax?
--Jacques

[-- Attachment #2: Type: text/html, Size: 160 bytes --]

Re: [Caml-list] polymorphic recursion

[Christophe TROESTLER]

On Mon, 12 May 2008 17:55:40 -0400, Jacques Le Normand wrote:
> 
> does ocaml support polymorphic recursion and, if so, what's the syntax?

Yes.  There are a couple of ways to make it work, using polymorphic
records or recursive modules.  You should check the archives of this
list for examples:

  http://groups.google.com/groups/dir?q=fa.caml

Cheers,
ChriS

Polymorphic recursion

[Loup Vaillant]

I was reading Okasaki's book, "Purely functionnal data structures",
and discovered that ML (and Ocaml) doesn't support non uniforms
function definitions.

So, even if:

(**)
type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
(**)

is correct,

(**)
let rec size = fun
   | Unit -> 0
   | Seq(_, b) -> 1 + 2 * size b;;
(**)

is not. Here is the error:
#
| Seq(_, b) -> 1 + 2 * size b;;
This expression (the last 'b') has type seq ('a * 'a) but is here used
with type seq 'a
#

Why?
Can't we design a type system which allow this "size" function?
Can't we implement non uniform recursive function (efficiently, or at all)?.

I suppose the problem is somewhat difficult, but I can't see where.

Regards,
Loup Vaillant

Re: [Caml-list] Polymorphic recursion

[Roland Zumkeller]

On 03/04/07, Loup Vaillant <loup.vaillant@gmail.com> wrote:
> Can't we implement non uniform recursive function (efficiently, or at all)?.

It has actually been done: call ocaml with the option "-rectypes" and
your example will work as is.

Best,

Roland

-- 
http://www.lix.polytechnique.fr/~zumkeller/

Re: [Caml-list] Polymorphic recursion

[Alain Frisch]

Roland Zumkeller wrote:
> On 03/04/07, Loup Vaillant <loup.vaillant@gmail.com> wrote:
>> Can't we implement non uniform recursive function (efficiently, or at
>> all)?.
> 
> It has actually been done: call ocaml with the option "-rectypes" and
> your example will work as is.

No. The example would typecheck and the following type will be inferred:

  val size : ('a * 'a as 'a) seq -> int = <fun>

but since there is no value of type ('a * 'a as 'a) (for some 'a), you
will be able to apply the function only to the value Unit:

# size Unit;;
- : int = 0
# size (Seq (1, Unit));;
This expression has type int * 'a seq but is here used with type
  ('b * 'b as 'b) * ('b * 'b) seq


This is a good illustration of why -rectypes is not enabled by default.


-- Alain

Re: Polymorphic recursion

[Stefan Monnier]

> This is a good illustration of why -rectypes is not enabled by default.

In my experience, polymorphic recursion is almost always linked to
datatypes whose recursion is itself polymorphic.  As is the case in
Loup's example.

Has there been work in trying to leverage this connection, so that
polymorphic recursion can be automatically inferred by taking advantage of
the implicit type hint provided by the datatype definition?


        Stefan

Polymorphic recursion

[Hongwei Xi]

Hi,

Could anyone tell me whether the feature of polymorphic
recursion is available in Caml-light or OCaml? If so,
how to use it (a simply example would suffice)?

Thanks,

--Hongwei

\~~~~/ \\   //  \\    //    @       Mail: hongwei@cse.ogi.edu
C-o^o,  ))__||   \\__//_  // \\     Url: http://www.cse.ogi.edu/~hongwei
(  ^ )  ))__||    \--/-\\     \\    Tel: +1 503 748 1584 (office)
/ \V\   ))  ||     //   \\     \\   Fax: +1 503 748 1553 (department)
------ //   || o  //     \\     \\// 
Department of Computer Science and Engineering
Oregon Graduate Institute of Science and Technology
P. O. Box 91000, Portland, OR 97291-1000, USA

Re: Polymorphic recursion

[Pierre Weis]

> Could anyone tell me whether the feature of polymorphic
> recursion is available in Caml-light or OCaml? If so,

Basically, the answer is no for the Caml-light or O'Caml
systems. Plans to add some form of polymorphic recursion is on the way.

For more details, have a look in the archive of this mailing list:

http://pauillac.inria.fr/caml/caml-list/subject.html

Subject: polymorphic recursion

Best regards,

Pierre Weis

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

polymorphic recursion

[Peter J Thiemann]

In some languages (most notably Haskell and Miranda) it is possible
to define a function that enjoys polymorphic recursion, i.e., the
types of its recursive calls may be instances of the type scheme at
which the function is defined.

For example:

let rec f x =
  let q = f true in
  let r = f 0 in
  x;;

is rejected by OCaml, but it is accepted by Haskell by saying

f :: a -> a
f x = let q = f True in
      let r = f 0 in
      x

Question:

Can you do the same in OCaml? I am aware of the tricks mentioned in
the FAQ, but I would like to know if there is a cleaner way to do it,
for example by providing a type signature.

-Peter

Re: polymorphic recursion

[Jacques GARRIGUE]

> In some languages (most notably Haskell and Miranda) it is possible
> to define a function that enjoys polymorphic recursion, i.e., the
> types of its recursive calls may be instances of the type scheme at
> which the function is defined.
> 
> Can you do the same in OCaml? I am aware of the tricks mentioned in
> the FAQ, but I would like to know if there is a cleaner way to do it,
> for example by providing a type signature.

To my knowledge, there is no direct way to do this. Part of the reason
is that type signatures have a different role in Haskell and ML: in
Haskell the type signature appears before its function, and restricts
it explicitely, while in ML you write it in an independent signature
file, which is not known when typing the function itself (signature
matching takes place after the type checking).

This does not matter very much in ML, since you explicitely decide
which functions recurse with which (in Haskell all definitions in a
module are a priori recursive), and there are only few examples really
needing polymorphic recursion.

To be complete on this point, in Objective Label method calls can be
polymorphically recursive:

# class r = object (self)
    method virtual m : 'a. 'a -> 'a
    method m x =
      let q = self#m true in
      let r = self#m 0 in
      x
  end;;
class r : object method m : 'a. 'a -> 'a end

Thanks to the mechanisms use for this inference, it would be easy to
provide polymorphic recursion for functions also, but we go back to
the ML problem: where do we write the signature ?

	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Re: polymorphic recursion

[Pierre Weis]

> To my knowledge, there is no direct way to do this. Part of the reason
> is that type signatures have a different role in Haskell and ML: in
[...]
> This does not matter very much in ML, since you explicitely decide
> which functions recurse with which (in Haskell all definitions in a
> module are a priori recursive), and there are only few examples really
> needing polymorphic recursion.

Yes, and for the excellent reason that you cannot use polymorphic
recursion in ML: this way it would be very surprising to find good
examples of its use, since nobody can write programs based on
polymorphic recursion!
 
> To be complete on this point, in Objective Label method calls can be
> polymorphically recursive:
> 
> # class r = object (self)
>     method virtual m : 'a. 'a -> 'a
>     method m x =
>       let q = self#m true in
>       let r = self#m 0 in
>       x
>   end;;
> class r : object method m : 'a. 'a -> 'a end
> 
> Thanks to the mechanisms use for this inference, it would be easy to
> provide polymorphic recursion for functions also, but we go back to
> the ML problem: where do we write the signature ?

Sintactically, it is easy: just the regular type constraint mechanism, writing:

let rec (f : 'a -> 'a) x =
 let q = f true in
 let r = f 0 in
 x;;

Unfortunately, the problem here is the semantics of type constraints
in ML: type constraints are not mandatory type assigment declarations,
but just annotations which should be compatible with the type infered
for the given expression. This means that a type constraint has to be
more general than the principal type of the annotated expression. For
instance, you can write:

let (f : 'a -> int) = function x -> x + 1;;
val f : int -> int = <fun>

Or :

let (f : 'a -> b) = function x -> x + 1;;
val f : int -> int = <fun>

Or even the most puzzling:

let (f : 'a) = function x -> x + 1;;
val f : int -> int = <fun>

This has many drawbacks, the most important being that no type
annotation in a program is reliable to the reader (except if the type
annotation does not posses any type variable at all).

If type constraints were mandatory, then the annotations will easily
give room to polymorphic recursion (the typechecker just acknowledges
the type annotation as the infered type and verifies the remaining
constraints). In my mind mandatory type annotations will be clearer
and more useful than the strange and almost useless semantics we have
now.

Polymorphic recursion via type annotations, while pratical and simple,
is not completely satisfactory: type inference of polymorphic
recursion would be much more in the spirit of ML. Unfortunately, this
problem, well-known as the ``mu-rule'' problem, has been proved
undecidable in general. However, a restricted kind of polymorphic
recursion inference is tractable (via semi-unification for
instance). Once upon a time, there were an old and wise Caml compiler
featuring such a restricted mechanism:

   CAML (sun4) (V3.1) by INRIA Fri Oct  1

#let rec f x =
# let q = f true in
# let r = f 0 in
# x;;
Value f is <fun> : 'a -> 'a

We still like this feature and we are still looking for a
tractable generalisation of this restricted polymorphic recursion
inference to add it to our new and strong compilers. Wait and see!

Pierre Weis

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

Re: polymorphic recursion

[Simon Helsen]

> Unfortunately, the problem here is the semantics of type constraints
> in ML: type constraints are not mandatory type assigment declarations,
> but just annotations which should be compatible with the type infered
> for the given expression. This means that a type constraint has to be
> more general than the principal type of the annotated expression. For

This might be the case for OCaml, but note that SML97 disallows more
general type-constraints than the type apparent in the expression without
the constraint (cf. rule (9) and comment in the 97 Definition - p22) 

> let (f : 'a -> int) = function x -> x + 1;;
> val f : int -> int = <fun>

in SML/NJ 110 this yields:

- val (f : 'a -> int) = fn x => x + 1;
stdIn:1.1-2.31 Error: pattern and expression in val dec don't agree
[literal]
  pattern:    'a -> int
  expression:    int -> int
  in declaration:
    f : 'a -> int = (fn x => x + 1)

> This has many drawbacks, the most important being that no type
> annotation in a program is reliable to the reader (except if the type
> annotation does not posses any type variable at all).

I suppose that this is exactly why Standard ML wants the type annotation
to have the exact degree of polymorphism as present in the expression. 

This makes sense in the filosophy that type constraints are only supposed
to be programmer documentation or to help the type-inference engine to
detect type-errors "earlier" (the latter is practical while debugging
type-errors).

Unfortunately, SML is not very consistent on this matter as well, since it
might require type annotations to succeed its type inference (e.g. at
top-level monomorphism and the resolution of variable record patterns) A
SML type-constraint cannot be more general, but is allowed to be more
specific. e.g:

- val (f : 'a -> 'a -> 'a) = fn x => fn y => y;
val f = fn : 'a -> 'a -> 'a

And if SML "would" follow this filosophy properly, there is no room for
polymorphic recursion in general since, as you indicate, type-inference
for this is undecidable. 

I don't know why Caml allows more general type constraints, but it might
be a good idea to follow SML on this matter (and I am interested to know
if there are good reasons for not doing this)

	Simon

----------------------- Simon Helsen ------------------------ 
--       Wilhelm-Schickard-Institut fuer Informatik        --
--           Arbeitsbereich Programmierung (PU)            --
--            Universitaet Tuebingen, Germany              --
-------------------------------------------------------------
-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

Re: polymorphic recursion

[Pierre Weis]

> This might be the case for OCaml, but note that SML97 disallows more
> general type-constraints than the type apparent in the expression without
> the constraint (cf. rule (9) and comment in the 97 Definition - p22) 

That's a good point. It's simple to state and understand.

> This makes sense in the filosophy that type constraints are only supposed
> to be programmer documentation or to help the type-inference engine to
> detect type-errors "earlier" (the latter is practical while debugging
> type-errors).

Yes, but furthermore it can be used to help the typechecker to find
types more general than it will normally find.

> Unfortunately, SML is not very consistent on this matter as well, since it
> might require type annotations to succeed its type inference (e.g. at
> top-level monomorphism and the resolution of variable record patterns) A
> SML type-constraint cannot be more general, but is allowed to be more
> specific. e.g:
> 
> - val (f : 'a -> 'a -> 'a) = fn x => fn y => y;
> val f = fn : 'a -> 'a -> 'a

This is necessary to ``constrain'' the types of programs, when you
want to obtain a type more specific than the one synthetized by
the typechecker, in order to get more precise typing
verifications. This is also useful to get rid of spurious type
unknowns at modules boundaries, since you cannot let them escape from
the module.

> And if SML "would" follow this filosophy properly, there is no room for
> polymorphic recursion in general since, as you indicate, type-inference
> for this is undecidable. 

Yes polymorphic recursion type-inference is undecidable.
No, ``exact'' type constraints do not preclude polymorphic recursion.

Starting with the ``exact'' type annotation as hypothesis, it is easy
to verify that the polymorphic recursion is sound. This is simple and
easy. The only drawback is that you have to find the type yourself,
and that you may indicate a too specific type.

> I don't know why Caml allows more general type constraints, but it might
> be a good idea to follow SML on this matter (and I am interested to know
> if there are good reasons for not doing this)

If we use it to get polymorphic recursion, there is a good reason to
do this.

Another problem is the scope of type variables in type
constraints. What's the meaning of

let f (x : 'a) (y : 'a) = y;;

We may need explicit Forall keywords to express type schemes in constraints.

Pierre Weis

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

Re: polymorphic recursion

[Simon Helsen]

> > I don't know why Caml allows more general type constraints, but it might
> > be a good idea to follow SML on this matter (and I am interested to know
> > if there are good reasons for not doing this)
> 
> If we use it to get polymorphic recursion, there is a good reason to
> do this.

right, but there is no polymorphic recursion in Ocaml, is there?

> Another problem is the scope of type variables in type
> constraints. What's the meaning of
> 
> let f (x : 'a) (y : 'a) = y;;
> 
> We may need explicit Forall keywords to express type schemes in constraints.

Indeed, this is a problem. Standard ML solves this by defining some
explicit rules for free type variables (section 4.6 of the definition -
p18) But, admitted, it's ugly and difficult. It would probably be better
to forbid free variables in type constraints altogether.

	Simon

----------------------- Simon Helsen ------------------------ 
--       Wilhelm-Schickard-Institut fuer Informatik        --
--           Arbeitsbereich Programmierung (PU)            --
--            Universitaet Tuebingen, Germany              --
-------------------------------------------------------------
-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

Re: polymorphic recursion

[Pierre Weis]

> right, but there is no polymorphic recursion in Ocaml, is there?

As mentioned earlier there is some form of polymorphic recursion in
objects. A (limited form of) polymorphic recursion could be added to
the core language in the future if we find a simple way to do so.

> > We may need explicit Forall keywords to express type schemes in constraints.
> 
> Indeed, this is a problem. Standard ML solves this by defining some
> explicit rules for free type variables (section 4.6 of the definition -
> p18).

As far as I know this rules do not allow the simple expression of polymorphic
type scheme in type constraints, since you have to figure out which
type variables are quantified and where they are bound (as far as I
remember this quantification implicitely occurs at the outermost level
of the construct where the type variable appears ?). Explicit
quantification would be simple and more explicit.

Pierre Weis

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

Re: polymorphic recursion

[Pierre CREGUT - FT.BD/CNET/DTL/MSV]

Quoting Pierre Weis (Pierre.Weis@inria.fr):
> > This might be the case for OCaml, but note that SML97 disallows more
> > general type-constraints than the type apparent in the expression without
> > the constraint (cf. rule (9) and comment in the 97 Definition - p22) 
> 
> That's a good point. It's simple to state and understand.
This way of handling type constraints is inherited from Hope.

[...]
> Another problem is the scope of type variables in type
> constraints. What's the meaning of
> 
> let f (x : 'a) (y : 'a) = y;;
> 
> We may need explicit Forall keywords to express type schemes in 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 :

  First un occurrence of 'a in a value declaration [val valbind] is said to
  be unguarded if the occurrence is not part of a smaller value declaration
  within [valbind]. In this case we say that 'a occurs unguarded in the value
  declaration. 

  Then we say that 'a is scoped at a particular occurrence O of [val valbind]
  in a  program if (1) 'a occurs unguarded in this value declaration, and (2)
   'a does not occur unguarded in any larger value declaration containing
  the occurrence O.

			Old Definition of Standard ML p 20

According to this definition, the 'a's denote the same type variable in
your example.

let g (x : 'a) = let f (x:'a) = x in x
let h (x : 'a) = x

is equivalent to 

let g (x : 'a) = let f (x:'a) = x in x
let h (x : 'b) = x

but not to 

let g (x : 'a) = let f (x:'c) = x in x
let h (x : 'b) = x

The only risk of this solution is that you overconstrain an expression 
because one of your type variable got caught in the scope of another unrelated
variable and then you get stuck with your compiler complaining about
a constraint it cannot fulfill. This is a safe risk.

-- 
Pierre Cregut - pierre.cregut@cnet.francetelecom.fr - +33 2 96 05 16 28
FT.CNET - DTL/MSV - 2 avenue Pierre Marzin - 22307 Lannion Cedex - France

Re: polymorphic recursion

[Xavier Leroy]

[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

Re: polymorphic recursion

[Pierre Weis]

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

In my mind the dark spot comes from the confusion between types and
type schemes due to the implicit quantification of type
variables. Writing ML programs, we need type schemes and not
types. Usual semantics for type annotations is ambiguous, since it
rely on strange rules to get rid of the absence of explicit
quantifiers in ML type schemes. Hence the strange semantics of
original ML (and CAML) type annotations: useless to the compiler and
useless to the reader of the program.

I suggest the following simple rules:

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

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

This is fairly conservative and easy to implement. For those
interested in details, I elaborate below on the consequences of this
two rules.


(I) What we gain:
=================

-- type constraints have a reliable meaning as type annotations in
programs,
-- polymorphic recursive definitions are easy to type check, if type
(scheme) annotated.

Examples:

let (f : int -> int) = function x -> x;;
Accepted:
--------
 int -> int is a valid type scheme for f (although not the most general one).
 f gets type (scheme) int -> int.

let (f : 'a -> 'b) = function x -> raise Not_found;;
Accepted:
---------
 'a -> 'b is a valid type scheme for f (the most general one).
 f gets type scheme Forall 'a 'b. 'a -> 'b

let (f : 'a -> 'a) = function x -> raise Not_found;;
Accepted:
---------
 'a -> 'a is a valid type scheme for f.
 f gets type scheme Forall 'a. 'a -> 'a

let (f : int -> int) = function x -> raise Not_found;;
Accepted:
---------
 int -> int is a valid type scheme for f.
 f gets type (scheme) int -> int.

let (f : 'a -> 'b) = function x -> x + 1;;
Rejected: 'a -> 'b is not a valid type scheme for f.
---------

let (f : 'a -> 'a) = function x -> x + 1;;
Rejected: 'a -> 'a is not a valid type scheme for f.
---------

The difference between this treatment and the actual semantics of type
annotations in Caml is fairly conservative: all the ``Accepted''
examples are already legal O'Caml programs and type assignments are
exactly the same. On the other hand, the strange ``Rejected''
annotations, that indeed use types that are more general than the
principal type scheme of the program, are now rejected.

(II) What we loose:
===================

As you may have noticed this new semantics precludes the sharing of
type variables between distinct type annotations. It is not clear to
me that this sharing is needed or really useful or desirable. Anyway,
this sharing is now impossible due to the new scope rule of type
variables, and to the type scheme interpretation of type annotations.
For instance, if we write:

let f (x : 'a) (y : 'a) = ...

meaning (according to the old semantics) that x and y should have the
same type, this is now rejected, since neither x nor y can be assigned
the polymorphic type scheme Forall 'a. 'a.

If we really need this sharing semantics we can use a
conservative extension of the basic scheme above, as follows:

(III) Extension to free type variables:
=======================================

To express type sharing between expressions, we must be able to express
constraints involving types with free type variables (not quantified
in any type scheme): we already have a notation to express those type
variables, namely '_a:

let f (x : '_a) (y : '_a) = x + y;;

Now the constraint is not quantified: it simply means that x and y should
have the same type (more precisely, it exists a type ty such that x :
ty and y : ty).

(The scope of these free type variables should be global to the phrase they
appear into and they can be assigned any type).

Pierre Weis

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

PS: We may also consider explicit Forall quantification in type
schemes. This is less conservative than this proposal but is
definitively clearer (furthermore, we get rid of this strange '_a
notation). Anyway, we may think we should have to introduce this
explicit quantification to support future extensions of the type
system to inner quantification; so it simpler to wait for these
extensions to introduce explicit quantification.

Re: polymorphic recursion

[Peter Thiemann]

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

Re: polymorphic recursion

[Pierre Weis]

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