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 SAA14824 for caml-redistribution; Tue, 22 Sep 1998 18:41: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 RAA29224 for ; Tue, 22 Sep 1998 17:50:27 +0200 (MET DST) Received: from p-voyageur.issy.cnet.fr (p-voyageur.issy.cnet.fr [139.100.0.39]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id RAA26236; Tue, 22 Sep 1998 17:50:25 +0200 (MET DST) Received: from l-mhs1.lannion.cnet.fr ([161.104.1.59]) by p-voyageur.issy.cnet.fr with SMTP (Microsoft Exchange Internet Mail Service Version 5.5.2232.9) id TAVPKR9Z; Tue, 22 Sep 1998 17:50:27 +0200 Received: from lsun564.lannion.cnet.fr ([161.104.10.181]) by l-mhs1.lannion.cnet.fr with SMTP (Microsoft Exchange Internet Mail Service Version 5.5.1960.3) id S9L5TF77; Tue, 22 Sep 1998 17:50:26 +0200 Received: by lsun564.lannion.cnet.fr (SMI-8.6/SMI-SVR4) id RAA15678; Tue, 22 Sep 1998 17:50:23 +0200 Message-ID: <19980922175023.23586@lsun564> Date: Tue, 22 Sep 1998 17:50:23 +0200 From: "Pierre CREGUT - FT.BD/CNET/DTL/MSV" To: Pierre Weis Cc: Simon Helsen , caml-list@inria.fr Subject: Re: polymorphic recursion References: <199809221506.RAA17926@pauillac.inria.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 0.88e In-Reply-To: <199809221506.RAA17926@pauillac.inria.fr>; from Pierre Weis on Tue, Sep 22, 1998 at 05:06:41PM +0200 Sender: weis 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