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 QAA09870 for caml-redistribution; Mon, 28 Sep 1998 16:28:26 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA03187 for ; Mon, 28 Sep 1998 15:00:39 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id PAA04890; Mon, 28 Sep 1998 15:00:36 +0200 (MET DST) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA32449; Mon, 28 Sep 1998 15:00:36 +0200 (MET DST) From: Pierre Weis Message-Id: <199809281300.PAA32449@pauillac.inria.fr> Subject: Re: polymorphic recursion To: pjt@cs.nott.ac.uk Date: Mon, 28 Sep 1998 15:00:36 +0200 (MET DST) Cc: caml-list@inria.fr In-Reply-To: <199809281145.MAA13917@polihale.cs.nott.ac.uk> from "Peter Thiemann" at Sep 28, 98 12:45:19 pm X-Mailer: ELM [version 2.4 PL24 ME8] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: 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/