English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    
Browse thread
ULTRA type error slicer for SML: version 0.6 and TECHNICAL REPORT
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: rahli vincent <vincent.rahli@g...>
Subject: ULTRA type error slicer for SML: version 0.6 and TECHNICAL REPORT
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 “./configure; make; make install” 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=0079

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