From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id E2368BC0A for ; Wed, 23 May 2007 07:21:59 +0200 (CEST) Received: from hugh.cs.washington.edu (hugh.cs.washington.edu [128.208.2.43]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l4N5Lvto002442 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Wed, 23 May 2007 07:21:59 +0200 Received: from [128.208.2.33] (gerald.cs.washington.edu [128.208.2.33]) by hugh.cs.washington.edu (8.14.1/8.14.1/1.9) with ESMTP id l4N5Lu4O025415; Tue, 22 May 2007 22:21:56 -0700 (envelope-from djg@cs.washington.edu) Message-ID: <4653CF5C.4040305@cs.washington.edu> Date: Tue, 22 May 2007 22:21:32 -0700 From: Dan Grossman User-Agent: Thunderbird 1.5.0.10 (Windows/20070221) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Cc: Ben Lerner Subject: Re: Teaching bottomline, part 3: what should improve. References: <20070522234715.0BCB2BC74@yquem.inria.fr> In-Reply-To: <20070522234715.0BCB2BC74@yquem.inria.fr> Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 4653CF75.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 ocaml:01 inference:01 implicitly:01 higher-order:01 pldi:01 pldi:01 wrote:01 caml:02 inferred:02 contributed:02 face:97 programming:03 languages:03 types:03 >> * Error messages of the type system are somewhat obscure. The reflex >> of many students is "OCaml wants it to be of type XXX", rather than >> "there is a contradiction in what I wrote". It would be nice if there >> was a way to ask OCaml to display additional information on type >> errors. > This is a long standing peeve of mine. Lets face it: Ocaml just lies. > If it has inferred a type, then finds a contradiction, it should > report both the location of the contradication AND all of the source > lines that contributed to the inference. Reporting all of the source lines has been investigated; see C. Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Science of Computer Programming, 50(1- 3):189–224, 2004. My intuition is there are many situations where this gives you too much information just as one location gives you too little. Switching to personal horn-tooting mode, you may be interested in a paper we have in PLDI next month where we take a completely different approach to presenting Caml type-errors -- we don't report any types at all, but rather we report a similar program that does type-check. See http://www.cs.washington.edu/homes/blerner/seminal.html. The PLDI paper is the place to start. The prototype implementation may prove useful to the very brave of heart, but it's really designed to demonstrate the idea. --Dan