A Type Error Slicer for MiniML

MiniML Grammar

• x ranges over variables.
• b ranges over boolean constants: true, false
• n ranges over integers: .., ~2, ~1, 0, 1, 2, ..

op ranges over the following binary infix operators:

  =, <, >, <=, >=, +, -, *, div, mod, @, o, andalso, orelse 
 

Initial environment:

  not, hd, tl, length, rev, map, foldr, foldl
 

decs ::=                        (empty decs) 
       | decs dec

dec ::= val pat = exp

      | val rec x = fn match

exp ::= x
      | b

      | if exp then exp else exp
      | n
      | exp op exp

      | ()
      | (exp1,...,expn)          n >= 1
      | fn match
      | exp exp

      | nil
      | exp :: exp
      | case exp of match
      | let decs in exp end


match ::= mrule
        | mrule | match

mrule ::= pat => exp

        
pat ::= _
      | x
      | b
      | n
      | ()
      | (pat1,...,patn)          n >= 1
      | nil
      | pat :: pat

Syntactic restrictions:

• Multiple occurrences of identical variables in patterns are disallowed.

TO DO

This is a work in progress. The following corrections and improvements are under consideration.

• Minimal type error slice highlighting issues:
  • For type constructor clash endpoints, maybe highlight instead the boundary between the penultimate node and the endpoint. That is, in "(fn x => if x then 1 else 2) 3", insert a colored boundary around the "3" and the "x". The latter boundary indicates that the if-then-else construct is the endpoint, but in particular the endpoint is reached via the condition subexpression rather than one of the other two expressions or via its return value.
  • The source code highlighting of "val x = (fn x => x + 1)(nil)" inserts a bizarre vertical bar in the middle of ")(". The same problem happens with "val _ = hd(1)". This is a bug.
  • Issues with the horizontal alignment of columns in the highlighted source code:
    • The use of bold font as part of the source code highlighting throws off the vertical alignment of columns because the browser apparently can pick a font with wider character cells. Is it sufficient to just change the background color?
    • The source code highlighting of "1true" and "(1)true" introduces a thin space with a border around it to mark the function application endpoint. This prevents columns from lining up.
    • The border around endpoints may be introducing a very small amount of space which prevents columns from lining up.
  • The top and bottom borders of the very thin function application endpoint marker in "1true" do not line up vertically with the other endpoint marker.
  • Use same highlighting scheme both for the separate slice and the full source code. This means that the non-".." portions of the separate slice should have a background color just like the highlighted source code. Also, the endpoint markers would look the same (would include the same whitespace). This will make it easier for the readers to see the commonality.
  • Use JavaScript to change the highlighting and displayed separate slices so that switching between error slices does not require loading a new web page.
  • Avoid using blue and gray backgrounds next to each other, because people with one kind of color-blindness can not distinguish this. The border around the endpoint helps, but may not be sufficient in general.
  • In "(1)true", the thin blue bar is nearly impossible to see next to the gray background behind the parenthesis. In "1true", the thin blue bar is merely hard to see. Maybe a brighter color could be used for endpoint that might be an application?
  • Provide interface option to allow inserting a bullet character to mark function application endpoints.
  • Support ability to select any subset of the error slices to highlight simultaneously on the same source code window. That is a bit hard to do with just HTML but can be done with HTML plus JavaScript. Also, this does not make sense in combination with a window showing just one of the slices separately.
• Textual explanation issues:
  • Write "unbound identifier" instead of "unbound variable" in the message to the user, because that is what most users will be accustomed to seeing.
  • Provide short textual explanation of "circularity" errors.
  • Add comments to beginning of each pre-supplied erroneous code example explaining what the example illustrates.
  • Provide better example names for the menu.
  • Add an explanation of the term "endpoint" somewhere for type constructor clashes.
  • Explain the highlighting of free variables in the legend.
  • Update the discussion at http://www.cee.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/doc/slices.html to be consistent with the current interface, e.g., add discussion of highlighting.
• Separate slice issues:
  • Stop the pretty printer from inserting extra redundant non-user-supplied parentheses in the separate slice. At least provide an interface option not to have them inserted.
  • Make the separate slice as similar as possible to the source code it was extracted from, i.e., it is desirable to maintain identical line breaks, use of parentheses, and columns of indentation. This will help the user map it onto their mental conception of their own source code.
  • Provide two different slices: the accurate slice, and a "compressed" one with reducible redexes removed. Include text explaining the difference.
• Supported language issues:
  • Allow the user to enter expressions (syntax derivable from the "exp" non-terminal in the SML grammar) rather than just declarations (syntax derivable from the "dec" non-terminal in the SML grammar).
  • Support more of SML. To handle all of SML, we need to have a parser for all of SML, write down the typing rules of SML in a new form, add typing rules for the derived constructs (these rules are not given in the SML definition), and extend the constraint solver to handle some additional sorts of constraints. In the short-term, high priority extensions include:
    • type annotations
    • the fun syntax
    • the [...] syntax for lists
    • real numbers (so that overloading errors can be shown)
  • Separate out the parser and pretty printer from the analysis engine.
  • Generalize tools to handle other languages.
• Web browser compatibility issues:
  • Warn the user they must enable CSS, colors, and fonts in their browser configuration in order to see the full effect.
  • Verify the output at least does not look horrible on bad web browsers as well as on incapable browsers like Lynx.
  • Document particular browsers that are known to have problems and also document some of the known problems.
  • Use another font where "list" does not look like "llst".
• Source code input issues:
  • Add more erroneous code examples from papers/type-error-slicing/example-output.
  • On the separate page with examples, provide a button next to each example to type check it, so the user does not have to paste it on the main page.
  • Provide an entry panel on each output page with the source code already filled in to allow the user to make fixes and check them quickly.
  • Provide an option that our tool will fetch the source code to be checked from a URL. This will be useful once we handle the full SML language.
  • Avoid using form entry fields on the page listing examples. Or include a comment explaining why we do this (to get whitespace treated properly when cutting and pasting) on the web page so that we don't look stupid.
  • Do something better when the code entry panel is empty.
• Investigate whether there is a good way to output minimal type error slices as they are discovered and then continue processing in the background looking for more.
• Fix the error message given when real numbers are entered.
• Give friendlier error messages for syntax errors in general.
• Arrange that the source code archive file is periodically updated with the latest source code.
• Make instructions in src/type-error-slicing-www/INSTALL file extremely explicit.
• Display the SML/NJ error message (for the pre-supplied examples) in a separate box.
• Show SML/NJ type error messages for user-supplied examples. Even better would be to also highlight the source-code region indicated by the SML/NJ error message. I don't know how to do this without running the security risk of evaluating arbitrary user-supplied code. Christian, do you know a way to just invoke the SML/NJ type checker?
• Set up our own web server on a less overloaded machine.
• Add more constraint labels to each syntactic form and use separate labels for each connection of an edge to a node. This will allow reporting the separate slice for (fn x => x nil) nil as (fn x => (.. x (..) ..)) nil instead of the current result of (fn x => x (..)) nil, which carries the misleading message that it is somehow important that x nil is the body of the function rather than merely somewhere inside the body.

We would be delighted to receive bug reports and suggestions. Please send them to Sébastien Carlier and Christian Haack.