From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 77DAFBC57 for ; Thu, 19 Aug 2010 16:10:35 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvABANvXbEzRVdi0kGdsb2JhbACGDJlmYQgVAQEBAQkJDAcRAx+iI4kYghOGQC6IVAEBAwWFMgSBVogb X-IronPort-AV: E=Sophos;i="4.56,233,1280700000"; d="scan'208";a="65875781" Received: from mail-qy0-f180.google.com ([209.85.216.180]) by mail1-smtp-roc.national.inria.fr with ESMTP; 19 Aug 2010 16:10:34 +0200 Received: by qyk31 with SMTP id 31so739472qyk.18 for ; Thu, 19 Aug 2010 07:10:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:date:message-id :subject:from:to:content-type; bh=RxoN26yF68oruDBy+KvZhWJthC18+oItO4U4Tx5U0x4=; b=O/V0YWhb4XZggICJNUI+7EreHp6y8m+bWNRq8g/WZONXehIZUufKanAj10M2csT16r JTuO1GQmyt1XKhLRSPl/wgwloLTgEJNuoyyGuKmK9r6FRHYSYqmD2MUB8b7OKJo0SO7J M5LdMx4En9mHlXizrdy7GoW+g5WMIQ/2xdhtU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=tkIATLForHlUZQh2MZJnfuhFfhaySZkl+fG35rRKkyj8YsMS70gQ0I1o2yBedbdoqp IP5CDPrrnhgVc3As51CZln2ajtrBeMDYM5IllXgiqykk5S1c2XIjLW4yFeqTUbaCZSiF DzemdwZEOsOlIl2/OrmPaTwgtBDj8i6+x41so= MIME-Version: 1.0 Received: by 10.229.217.207 with SMTP id hn15mr7284999qcb.165.1282227032820; Thu, 19 Aug 2010 07:10:32 -0700 (PDT) Received: by 10.229.32.133 with HTTP; Thu, 19 Aug 2010 07:10:32 -0700 (PDT) Date: Thu, 19 Aug 2010 15:10:32 +0100 Message-ID: Subject: ULTRA type error slicer for SML: version 0.6 and TECHNICAL REPORT From: rahli vincent To: caml-list@yquem.inria.fr Content-Type: multipart/alternative; boundary=0016361e88c4d00bc8048e2dbe1e X-Spam: no; 0.00; ill-typed:01 elegantly:01 functors:01 functors:01 unpack:01 infix:01 inference:01 emacs:01 checker:01 ill-typed:01 elegantly:01 unpack:01 infix:01 inference:01 emacs:01 --0016361e88c4d00bc8048e2dbe1e Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable We are happy to announce the release of two things: * Technical report HW-MACS-TR-0079 "A constraint system for a SML type error slicer" which explains how our type error slicing software works. * The new version 0.6 of our type error slicing software for the SML programming language. The abstract of the technical report is: Existing compilers for many languages have confusing type error messages. Type error slicing (TES) helps the programmer by isolating the part of a program contributing to a type error, but unfortunately TES was initially done for a tiny toy language. Extending TES to a full programming language is extremely challenging, and for SML we needed a number of innovations and generalisations. Some issues would be faced for any language, and some are SML-specific but representative of the complexity of language-specific issues likely to be faced for other languages. We solve both kinds of issues and present a simple, general constraint system for providing type error slices for ill-typed programs. Our constraint system elegantly and efficiently handles features like the intricate "open" SML feature. We show how the simple clarity of type error slices can demystify language features known to confuse users. We also provide in an appendix a case study on how to use TES to help modifying user data types, and extend the core language presented in the main body of this report to handle more of the implementation of our system. These extensions allow handling local declarations, type declarations and some uses of signatures. Regarding the software, major improvements over the previous release include: * The slicer is 10 to 100 times faster in many cases, and can reasonably be used on programs containing 10 thousand lines of code. * We support some uses of functors (that is, we report some type errors involving functors). * We report more kinds of errors and the error messages have been improved. * We provide a source archive (that is, a .tar.gz file which you unpack and run =93./configure; make; make install=94 in the unpacked directory). Other less important improvement is: * The slicer now quickly sends non-minimal error slices to the user interface and then sends a minimal replacement error slice after doing more time-consuming work. * We partially support fixity declarations in that we parse and type check programs using them correctly. Highlighting of infix declarations and identifiers in error slices is not yet correct. Even more changes are documented in the ChangeLog file. The aim of our type error slicer is to provide useful type error reports for pieces of code written in SML: * It identifies all of the program points that contribute to a type error, including the spot with the actual programming error that caused the type error. * It highlights these program points in the original, unchanged source code. * It avoids showing internal details of the operation of the type inference machinery. A new source archive and new Ubuntu (Debian based) and Fedora (Red-Hat based) packages of our type error slicer can be found at this URL: http://www.macs.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/ The technical report can be found at this URL: http://www.macs.hw.ac.uk:8080/techreps/view_record.jsp?id=3D0079 Known limitations: * We have not yet built the software for other operating systems than Linux. * The currently supported user interfaces are via a terminal window, GNU Emacs (or our web demo). We are currently developing a Vim interface. * Some type errors are not yet discovered (the user will need to rely on their usual type checker in these cases). Notable spots where the implementation is incomplete are equality types and sharing constraints. * The details of the SML basis library are incomplete (fortunately the user can add any additional details they are using). Best wishes, Vincent Rahli and Joe Wells --0016361e88c4d00bc8048e2dbe1e Content-Type: text/html; charset=windows-1252 Content-Transfer-Encoding: quoted-printable We are happy to announce the release of two things:

=A0 * Technical = report HW-MACS-TR-0079 "A constraint system for a SML
=A0=A0=A0 typ= e error slicer" which explains how our type error
=A0=A0=A0 slicing= software works.
=A0 * The new version 0.6 of our type error slicing software for the SML=A0=A0=A0 programming language.

The abstract of the technical repor= t is:

=A0=A0=A0 Existing compilers for many languages have confusing= type error
=A0=A0=A0 messages.=A0 Type error slicing (TES) helps the programmer by
= =A0=A0=A0 isolating the part of a program contributing to a type error, but=
=A0=A0=A0 unfortunately TES was initially done for a tiny toy language.=
=A0=A0=A0 Extending TES to a full programming language is extremely
=A0=A0=A0 challenging, and for SML we needed a number of innovations and=A0=A0=A0 generalisations.=A0 Some issues would be faced for any language,= and
=A0=A0=A0 some are SML-specific but representative of the complexit= y of
=A0=A0=A0 language-specific issues likely to be faced for other lan= guages.
=A0=A0=A0 We solve both kinds of issues and present a simple, general
= =A0=A0=A0 constraint system for providing type error slices for ill-typed=A0=A0=A0 programs.=A0 Our constraint system elegantly and efficiently ha= ndles
=A0=A0=A0 features like the intricate "open" SML feature= .=A0 We show how the
=A0=A0=A0 simple clarity of type error slices can demystify language
=A0= =A0=A0 features known to confuse users.

=A0=A0=A0 We also provide in= an appendix a case study on how to use TES to
=A0=A0=A0 help modifying = user data types, and extend the core language
=A0=A0=A0 presented in the main body of this report to handle more of the=A0=A0=A0 implementation of our system.=A0 These extensions allow handlin= g
=A0=A0=A0 local declarations, type declarations and some uses of signa= tures.


Regarding the software, major improvements over the previous release
inc= lude:
=A0 * The slicer is 10 to 100 times faster in many cases, and can<= br>=A0=A0=A0 reasonably be used on programs containing 10 thousand lines of=
=A0=A0=A0 code.
=A0 * We support some uses of functors (that is, we repo= rt some type
=A0=A0=A0 errors involving functors).
=A0 * We report mo= re kinds of errors and the error messages have been
=A0=A0=A0 improved.<= br>=A0 * We provide a source archive (that is, a .tar.gz file which you
=A0=A0=A0 unpack and run =93./configure; make; make install=94 in the unpac= ked
=A0=A0=A0 directory).

Other less important improvement is:=A0 * The slicer now quickly sends non-minimal error slices to the user=A0=A0=A0 interface and then sends a minimal replacement error slice after=
=A0=A0=A0 doing more time-consuming work.
=A0 * We partially support fix= ity declarations in that we parse and type
=A0=A0=A0 check programs usin= g them correctly.=A0 Highlighting of infix
=A0=A0=A0 declarations and id= entifiers in error slices is not yet correct.

Even more changes are documented in the ChangeLog file.

The aim = of our type error slicer is to provide useful type error
reports for pie= ces of code written in SML:
=A0 * It identifies all of the program point= s that contribute to a type
=A0=A0=A0 error, including the spot with the actual programming error that<= br>=A0=A0=A0 caused the type error.
=A0 * It highlights these program po= ints in the original, unchanged
=A0=A0=A0 source code.
=A0 * It avoid= s showing internal details of the operation of the type
=A0=A0=A0 inference machinery.

A new source archive and new Ubuntu (= Debian based) and Fedora (Red-Hat
based) packages of our type error slic= er can be found at this URL:
=A0 http://www.macs.hw.ac.uk/ult= ra/compositional-analysis/type-error-slicing/

The technical report can be found at this URL:
=A0 http://www.macs= .hw.ac.uk:8080/techreps/view_record.jsp?id=3D0079

Known limitati= ons:
=A0 * We have not yet built the software for other operating systems
=A0= =A0=A0 than Linux.
=A0 * The currently supported user interfaces are via= a terminal window,
=A0=A0=A0 GNU Emacs (or our web demo).=A0 We are cur= rently developing a Vim
=A0=A0=A0 interface.
=A0 * Some type errors are not yet discovered (the = user will need to
=A0=A0=A0 rely on their usual type checker in these ca= ses).=A0 Notable spots
=A0=A0=A0 where the implementation is incomplete = are equality types and
=A0=A0=A0 sharing constraints.
=A0 * The details of the SML basis librar= y are incomplete (fortunately
=A0=A0=A0 the user can add any additional = details they are using).


Best wishes,

Vincent Rahli and J= oe Wells
--0016361e88c4d00bc8048e2dbe1e--