**Next message:**Pierre Weis: "Re: polymorphic recursion"**Previous message:**Pierre Weis: "Re: polymorphic recursion"**Maybe in reply to:**Peter J Thiemann: "polymorphic recursion"**Next in thread:**Pierre Weis: "Re: polymorphic recursion"**Reply:**Pierre Weis: "Re: polymorphic recursion"**Reply:**Andrew Kay: "OCaml infix function-composition"**Reply:**Vyskocil Vladimir: "Marshaling pour les objets ?"**Reply:**Damien Doligez: "Objective Caml on MacOS"**Reply:**Serge Fantino: "porté des définitions des variables de classe"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

Message-Id: <199809281145.MAA13917@polihale.cs.nott.ac.uk>

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

Subject: Re: polymorphic recursion

Date: Mon, 28 Sep 1998 12:45:19 +0100

From: 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

**Next message:**Pierre Weis: "Re: polymorphic recursion"**Previous message:**Pierre Weis: "Re: polymorphic recursion"**Maybe in reply to:**Peter J Thiemann: "polymorphic recursion"**Next in thread:**Pierre Weis: "Re: polymorphic recursion"**Reply:**Pierre Weis: "Re: polymorphic recursion"**Reply:**Andrew Kay: "OCaml infix function-composition"**Reply:**Vyskocil Vladimir: "Marshaling pour les objets ?"**Reply:**Damien Doligez: "Objective Caml on MacOS"**Reply:**Serge Fantino: "porté des définitions des variables de classe"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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