**Next message:**Peter Thiemann: "Re: polymorphic recursion"**Previous message:**Daniel de Rauglaudre: "Re: Ocaml users outside France (and inside too)"**Next in thread:**Anton Moscal: "Local definitions"**Reply:**Anton Moscal: "Local definitions"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

From: Pierre Weis <Pierre.Weis@inria.fr>

Message-Id: <199809280951.LAA27562@pauillac.inria.fr>

Subject: Re: polymorphic recursion

To: leroy@welcome.disi.unige.it (Xavier Leroy)

Date: Mon, 28 Sep 1998 11:51:09 +0200 (MET DST)

In-Reply-To: <19980922191410.C17087@welcome.disi.unige.it> from "Xavier Leroy" at Sep 22, 98 07:14:10 pm

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

**Next message:**Peter Thiemann: "Re: polymorphic recursion"**Previous message:**Daniel de Rauglaudre: "Re: Ocaml users outside France (and inside too)"**Next in thread:**Anton Moscal: "Local definitions"**Reply:**Anton Moscal: "Local definitions"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b29
: Sun Jan 02 2000 - 11:58:16 MET
*