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 QAA28710 for caml-redistribution; Tue, 22 Sep 1998 16:39:39 +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 MAA03237 for ; Tue, 22 Sep 1998 12:00:16 +0200 (MET DST) Received: from macon.informatik.uni-tuebingen.de (macon2.Informatik.Uni-Tuebingen.De [134.2.13.2]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id MAA20967; Tue, 22 Sep 1998 12:00:13 +0200 (MET DST) Received: from modas.informatik.uni-tuebingen.de (modas.Informatik.Uni-Tuebingen.De [134.2.12.3]) by macon.informatik.uni-tuebingen.de (8.9.1/8.9.1) with SMTP id MAA10708; Tue, 22 Sep 1998 12:00:14 +0200 Received: from localhost by modas.informatik.uni-tuebingen.de (AIX 4.1/UCB 5.64/4.03) id AA26530; Tue, 22 Sep 1998 12:00:11 +0200 Date: Tue, 22 Sep 1998 12:00:11 +0200 (MST) From: Simon Helsen X-Sender: helsen@modas To: Pierre Weis Cc: Caml Mailing-list Subject: Re: polymorphic recursion In-Reply-To: <199809220922.LAA11296@pauillac.inria.fr> Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: weis > Unfortunately, the problem here is the semantics of type constraints > in ML: type constraints are not mandatory type assigment declarations, > but just annotations which should be compatible with the type infered > for the given expression. This means that a type constraint has to be > more general than the principal type of the annotated expression. For 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) > let (f : 'a -> int) = function x -> x + 1;; > val f : int -> int = in SML/NJ 110 this yields: - val (f : 'a -> int) = fn x => x + 1; stdIn:1.1-2.31 Error: pattern and expression in val dec don't agree [literal] pattern: 'a -> int expression: int -> int in declaration: f : 'a -> int = (fn x => x + 1) > This has many drawbacks, the most important being that no type > annotation in a program is reliable to the reader (except if the type > annotation does not posses any type variable at all). I suppose that this is exactly why Standard ML wants the type annotation to have the exact degree of polymorphism as present in the expression. 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). 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 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. 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) Simon ----------------------- Simon Helsen ------------------------ -- Wilhelm-Schickard-Institut fuer Informatik -- -- Arbeitsbereich Programmierung (PU) -- -- Universitaet Tuebingen, Germany -- ------------------------------------------------------------- -- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --