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