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 LAA04409 for caml-redistribution@pauillac.inria.fr; Fri, 11 Feb 2000 11:18:17 +0100 (MET) Resent-Message-Id: <200002111018.LAA04409@pauillac.inria.fr> 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 LAA15190 for ; Fri, 11 Feb 2000 11:17:52 +0100 (MET) 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 LAA27386; Fri, 11 Feb 2000 11:17:49 +0100 (MET) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA18181; Fri, 11 Feb 2000 11:17:49 +0100 (MET) Message-ID: <20000211111749.34427@pauillac.inria.fr> Date: Fri, 11 Feb 2000 11:17:49 +0100 From: Pierre Weis To: jean-marc alliot Cc: caml-list@inria.fr Subject: Re: Typing problem References: <38A2C1E3.1CF1AFFC@recherche.enac.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 0.89.1 In-Reply-To: <38A2C1E3.1CF1AFFC@recherche.enac.fr>; from jean-marc alliot on Thu, Feb 10, 2000 at 02:49:23PM +0100 Resent-From: weis@pauillac.inria.fr Resent-Date: Fri, 11 Feb 2000 11:18:17 +0100 Resent-To: caml-redistribution@pauillac.inria.fr > We recently found a quite annoying problem with the typing system in > ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other > people might be be interested however. > > The problem is summarized in the following code: > > First let's define two types: > type t1 = (?l:int -> unit -> unit) > type t = Toto of t1 > > Then the function: > let f1 g = > g l:3 (); > (Toto g);; > > This function doesn't compile and the compiler error message is somewhat > cryptic at first sight: > File "toto.ml", line 11, characters 8-9: > This expression has type int -> unit -> 'a but is here used with type > t1 = ?l:int -> unit -> unit Thank you very much for pointing out this interesting problem: I'm sure there is room for improvement here for our new label compiler. If you use the -modern option of the compiler you would get a much clearer message, namely: # let f1 g = g l:3 (); (Toto g);; This expression has type l:int -> unit -> 'a but is here used with type t1 = ?l:int -> unit -> unit This clearly states that the optional status of the label is involved in the problem. Hence, a language level fix could simply be to allow the user to write the question mark with the label as: let f1 g = g ?l:3 (); (Toto g);; Now, in conjontion with the -modern option, this would be perfectly clear to understand why g l:3 is rejected while g ?l:3 is not. Unfortunately, this last program is not yet handled properly by the compiler, since it causes an assertion failure into the typechecker: # let f1 g = g ?l:3 (); (Toto g);; This expression has type ?l:Uncaught exception: File "typing/printtyp.ml", line 0, characters 6649-6661: Assertion failed > We would very much like to see this clearly documented in ocaml 2.99 > reference manual, as it is a serious change in the behavior of the > typing system. Determinism is lost, as typing f1 would succeed if typing > was done in reverse order (from last line to first line). > Perhaps also a different error message from the compiler would help in > detecting such problems. I don't think that determinism is lost, in the sense that the compiler always output the same answers! But you're right to mention that this would be another way to test in which order in which the type-checker type-checks the sub-expressions of a program. You're also right in that we always would like better and better error messages, I would say particularly for the last program I wrote: we would very much like the compiler not to fail to print the error report! No doubt that this erroneous error message will be corrected before the experimental 2.99 version will turn into a stable 3.0 version of Objective Caml. Also, may be Jacques could tell us what is his opinion about the optional labels status in expressions (as in g ?l:3). Best regards, -- Pierre Weis INRIA, Projet Cristal, http://pauillac.inria.fr/~weis