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 RAA10375 for caml-redistribution; Tue, 22 Sep 1998 17:07:19 +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 RAA06679 for ; Tue, 22 Sep 1998 17:06:44 +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 RAA22021; Tue, 22 Sep 1998 17:06:41 +0200 (MET DST) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA17926; Tue, 22 Sep 1998 17:06:41 +0200 (MET DST) From: Pierre Weis Message-Id: <199809221506.RAA17926@pauillac.inria.fr> Subject: Re: polymorphic recursion To: helsen@informatik.uni-tuebingen.de (Simon Helsen) Date: Tue, 22 Sep 1998 17:06:41 +0200 (MET DST) Cc: caml-list@inria.fr In-Reply-To: from "Simon Helsen" at Sep 22, 98 12:00:11 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 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 makes sense in the filosophy that type constraints are only supposed > to be programmer documentation or to help the type-inference engine to > detect type-errors "earlier" (the latter is practical while debugging > type-errors). Yes, but furthermore it can be used to help the typechecker to find types more general than it will normally find. > Unfortunately, SML is not very consistent on this matter as well, since it > might require type annotations to succeed its type inference (e.g. at > top-level monomorphism and the resolution of variable record patterns) A > SML type-constraint cannot be more general, but is allowed to be more > specific. e.g: > > - val (f : 'a -> 'a -> 'a) = fn x => fn y => y; > val f = fn : 'a -> 'a -> 'a This is necessary to ``constrain'' the types of programs, when you want to obtain a type more specific than the one synthetized by the typechecker, in order to get more precise typing verifications. This is also useful to get rid of spurious type unknowns at modules boundaries, since you cannot let them escape from the module. > And if SML "would" follow this filosophy properly, there is no room for > polymorphic recursion in general since, as you indicate, type-inference > for this is undecidable. Yes polymorphic recursion type-inference is undecidable. No, ``exact'' type constraints do not preclude polymorphic recursion. Starting with the ``exact'' type annotation as hypothesis, it is easy to verify that the polymorphic recursion is sound. This is simple and easy. The only drawback is that you have to find the type yourself, and that you may indicate a too specific type. > I don't know why Caml allows more general type constraints, but it might > be a good idea to follow SML on this matter (and I am interested to know > if there are good reasons for not doing this) If we use it to get polymorphic recursion, there is a good reason to do this. 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. Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/