From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA18637; Fri, 7 Jun 2002 09:07:51 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 JAA18613 for ; Fri, 7 Jun 2002 09:07:50 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g5777oH00443 for ; Fri, 7 Jun 2002 09:07:50 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA18615 for caml-list@inria.fr; Fri, 7 Jun 2002 09:07:50 +0200 (MET DST) Date: Fri, 7 Jun 2002 09:07:50 +0200 From: Francois Pottier To: caml-list@inria.fr Subject: Re: [Caml-list] Comments on type variables Message-ID: <20020607090750.B17859@pauillac.inria.fr> Reply-To: Francois.Pottier@inria.fr References: Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 1.0i In-Reply-To: ; from frisch@clipper.ens.fr on Thu, Jun 06, 2002 at 07:04:48PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Alain, You are right -- the way type variable names are introduced and managed is a mess in O'Caml. I (could be wrong but I) don't think much thought was ever given to this aspect of the language. It would be possible to have constructs to introduce such type names, with lexical scope, at any point within an expression. It would also be possible to give such names existential or universal meaning. That is, we could have two expression forms exists 'a in e forall 'a in e In both cases, 'a is bound within e. In the former case, it may be instantiated to any type, while in the latter case, it must remain polymorphic within e. Currently O'Caml only gives existential meaning to type variables, as you notice. I don't think it would be difficult to implement these constructs. The required machinery, I believe, has already been introduced in order to support local modules (`let module'). I could be wrong, since I'm not familiar with O'Caml's typechecker. > Interaction with local modules > ------------------------------ > > Inside a local module, type variables introduced outside the module are > invisible: > > # let f (x : 'a) = > let module M = struct type t = 'a list end in ();; > Unbound type parameter 'a I would call it a bug, and a very annoying one. > '_a variables > ------------- > > It is not possible to specify "impure" type variables: > > # let z = let g y = y in g [];; > val z : '_a list = [] > # let z : '_a list = [];; > val z : 'a list = [] There is no such thing as an "impure" type variable. A much cleaner notion is that of an variable which has been (existentially) bound somewhere higher up. For instance, instead of writing > # module M = (struct let x = ref [] end : sig val x : '_a list ref end);; you could write # exists 'a # module M = (struct let x = ref [] end : sig val x : 'a list ref end) (I'm using here a toplevel variant of the `exists 'a in e' expression form.) Here, 'a is explicitly introduced at a certain point, and it is then referenced in the signature. This looks perfectly fine to me; the only problem is that it must be clear that 'a is not locally universally quantified in the signature, and this requires either that universal quantifiers be explicitly listed in signatures (cumbersome) or that any type names which happen to be in scope *not* be considered as implicitly locally universally quantified. (I don't know if I'm being clear enough, but I can clarify if there's interest.) > Variable name in error message > ------------------------------ > > Error messages would be more readable if they retained (when possible) > variable names: > > # let f (a : 'a) (b : 'b list) = b + 1;; > This expression has type 'a list but is here used with type int The (early prototype) implementation of my toy language does this, at least for variable names introduced by `forall'. So you can type: let forall a b . f (a :: a) (b :: list b) = b + 1 *** Error: int = list b It makes sense to keep track of names for variables introduced with universal meaning, because they will never be unified with some other variable, so they really have their own identity, in a way. For those variables introduced by with existential meaning, it would be more problematic; these variables are typically unified with arbitrary types. These issues are discussed in a recent paper by Peyton Jones and Shields, which is worth reading; see http://research.microsoft.com/Users/simonpj/papers/scoped-tyvars/ -- François Pottier Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/ ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners