From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 779AD7FD90 for ; Tue, 10 Jan 2017 11:45:19 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.33,343,1477954800"; d="scan'208,217";a="208602158" Received: from unknown (HELO [130.79.192.245]) ([130.79.192.245]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 10 Jan 2017 11:45:19 +0100 To: caml-list@inria.fr From: =?UTF-8?Q?Arthur_Chargu=c3=a9raud?= Message-ID: Date: Tue, 10 Jan 2017 11:45:18 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="------------9CFE7B3537B871C4417BD6E7" Subject: [Caml-list] Improved type error messages for Ocaml This is a multi-part message in MIME format. --------------9CFE7B3537B871C4417BD6E7 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Dear OCaml users, It is my pleasure to announce the beta release of my patch for improved type error messages. | opam switch 4.02.2+improved-errors| Quick demo: *** With "ocamlc" *** let _ = List.map (fun x -> x + 1) [2.0; 3.0] ^^^ Error: This expression has type float but an expression was expected of type int. This message is very confusing to the user who intented to write: (fun x -> x +. 1.) *** With "ocamlc -easy-type-errors" *** let _ = List.map (fun x -> x + 1) [2.0; 3.0] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The function `List.map' cannot be applied to the arguments provided. | Types of the expected arguments: | Types of the provided arguments: ---|-------------------------------------|------------------------------------ 1 | 'a -> 'b | int -> int 2 | 'a list | float list This new message show all the types involved, and does not attempt to guess whether the user intended to write [2; 3] or intended to write (fun x -> x +. 1.); Trying to guess is a bad idea, because roughly half of the time the guess is wrong, and it just adds more confusion. Many more (cool) demos are available from the following sources: * paper: http://www.chargueraud.org/research/2015/ocaml_errors/ocaml_errors.pdf * slides: http://www.chargueraud.org/talks/2014_09_05_talk_ocaml_errors.pdf * video: https://www.youtube.com/watch?v=V_ipQZeBueg How it works (short version): When the flag "-easy-type-errors" is activated, the compiler behaves exactly as usual, except when a top level definition fails to type-check. At such point, the definition is type-checked again, using a slightly modified unification algorithm, able to produce messages that are (I argue) more informative for locating the error. The patched compiler is thus able to provide alternative error messages with zero performance overhead on successful compilations. For ill-typed programs, the new typing algorithm may be slightly slower than the original one (as it performs a larger number of generalizations), but it should never be orders of magnitude slower. Pretty much all of OCaml is supported, with the notable exceptions of GADTs (by lack of time of expertise), and record field name overloading (due to the fact that it depends on the order in which unifications are performed). Note that top-level definitions involving such features will still compile properly, as long as it they do not contain any type error; if they do, then the error message will likely be uninformative, in which case the flag "-easy-type-errors" needs to be turned off. If you like this patch and would like to see it one day integrated in the main distribution, please post feedback on the mailing list, to convince the developers and myself that it is worth further investment. I am especially interested in feedback on the use of the new error messages in the context of teaching OCaml. Enjoy! + Arthur [Many thanks to Armaël Guéneau and Gabriel Scherer for their help with the opam packaging.] --------------9CFE7B3537B871C4417BD6E7 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit Dear OCaml users,


It is my pleasure to announce the beta release of my patch for improved type error messages.

    opam switch 4.02.2+improved-errors


Quick demo:

*** With "ocamlc" ***


 let _ = List.map (fun x -> x + 1) [2.0; 3.0]
                                   ^^^
 Error: This expression has type float but an expression was expected of type int.

This message is very confusing to the user who intented to write: (fun x -> x +. 1.)


*** With "ocamlc -easy-type-errors" ***


let _ = List.map (fun x -> x + 1) [2.0; 3.0]
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
Error: The function `List.map' cannot be applied to the arguments provided.

   | Types of the expected arguments:    | Types of the provided arguments:
---|-------------------------------------|------------------------------------
 1 | 'a -> 'b                            | int -> int
 2 | 'a list                             | float list


This new message show all the types involved, and does not attempt to guess whether the user intended to write  [2; 3]  or intended to write  (fun x -> x +. 1.); Trying to guess is a bad idea, because roughly half of the time the guess is wrong, and it just adds more confusion.



Many more (cool) demos are available from the following sources:


How it works (short version):

When the flag "-easy-type-errors" is activated, the compiler behaves exactly as usual, except when a top level definition fails to type-check. At such point, the definition is type-checked again, using a slightly modified unification algorithm, able to produce messages that are (I argue) more informative for locating the error. The patched compiler is thus able to provide alternative error messages with zero performance overhead on successful compilations. For ill-typed programs, the new typing algorithm may be slightly slower than the original one (as it performs a larger number of generalizations), but it should never be orders of magnitude slower.

Pretty much all of OCaml is supported, with the notable exceptions of GADTs (by lack of time of expertise), and record field name overloading (due to the fact that it depends on the order in which unifications are performed). Note that top-level definitions involving such features will still compile properly, as long as it they do not contain any type error; if they do, then the error message will likely be uninformative, in which case the flag "-easy-type-errors" needs to be turned off.


If you like this patch and would like to see it one day integrated in the main distribution, please post feedback on the mailing list, to convince the developers and myself that it is worth further investment. I am especially interested in feedback on the use of the new error messages in the context of teaching OCaml.


Enjoy!

+
Arthur

[Many thanks to Armaël Guéneau and Gabriel Scherer for their help with the opam packaging.]


--------------9CFE7B3537B871C4417BD6E7--