Re: Typing problem

From: Pierre Weis (Pierre.Weis@inria.fr)
Date: Fri Feb 11 2000 - 11:17:49 MET

  • Next message: Markus Mottl: ""catch-all" labels?"

    > 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



    This archive was generated by hypermail 2b29 : Fri Feb 11 2000 - 11:20:47 MET