From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: weis Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA22690 for caml-redistribution; Mon, 28 Sep 1998 15:01:09 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id NAA12129 for ; Mon, 28 Sep 1998 13:45:22 +0200 (MET DST) Received: from polihale.cs.nott.ac.uk (polihale.cs.nott.ac.uk [128.243.20.139]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id NAA20378; Mon, 28 Sep 1998 13:45:20 +0200 (MET DST) Received: from polihale.cs.nott.ac.uk (localhost [127.0.0.1]) by polihale.cs.nott.ac.uk (8.8.7/8.8.7) with ESMTP id MAA13917; Mon, 28 Sep 1998 12:45:19 +0100 (BST) (envelope-from pjt@polihale.cs.nott.ac.uk) Message-Id: <199809281145.MAA13917@polihale.cs.nott.ac.uk> To: Pierre Weis cc: Xavier Leroy , caml-list@inria.fr Subject: Re: polymorphic recursion In-reply-to: (Your message of Mon, 28 Sep 1998 11:51:09 +0200.) <199809280951.LAA27562@pauillac.inria.fr> References: <199809280951.LAA27562@pauillac.inria.fr> Comments: Hyperbole mail buttons accepted, v04.023. Reply-To: pjt@cs.nott.ac.uk cc: pjt@cs.nott.ac.uk Mime-Version: 1.0 (generated by tm-edit 7.108) Content-Type: text/plain; charset=US-ASCII Date: Mon, 28 Sep 1998 12:45:19 +0100 From: Peter Thiemann Sender: weis >>>>> "Pierre" == Pierre Weis 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