jstolarek / slicer

Companion code for paper "Imperative Functional Programs that Explain their Work", Wilmer Ricciotti, Jan Stolarek, Roly Perera and James Cheney, ICFP 2017, Oxford, UK
http://dl.acm.org/citation.cfm?id=3110258
GNU General Public License v3.0
6 stars 0 forks source link

Better error pretty-printing #24

Open jstolarek opened 7 years ago

jstolarek commented 7 years ago

Right now, when throwing an error we don't pretty print the offending expressions but simply show the syntax tree, eg.:

desugarM (A.Deref e)
    = do (e', ty) <- desugarM e
         unless (isRefTy ty) $
                desugarError ("Dereferenced expression (" ++ show e ++
                             ") does not have a reference type")
         return (EDeref e', fstTy ty)

We could do better by resugaring and pretty-printing expressions in error messages, but that is a bit tricky. At the moment we can go from values and core expressions into resugared syntax. The resugaring function, however, is partial. So if the expression is ill-formed and does not type-check then most likely it will also cause a resugaring error. I believe this can be solved easily by adding a desugaring from surface syntax into resugared syntax - it should be possible then to write a total resugaring function that would be safe to use when throwing an error. Oh, and we're also throwing errors during evaluation. But expressions that are evaluated should be well-typed and thus, hopefully, safe to resugar (that's wishful thinking here - haven't checked!).

It might also be worth to:

  1. Define a type class for data types that can be resugared:

      class Resugarable a where
         resugar :: a -> DesugarM RExp
  2. Create a function pp :: Pretty a => a -> DesugarM String - explicit calls to show are a bit tedious.

jstolarek commented 7 years ago

This seems to be a very low priority. During desugaring and evaluation there is only a handful of situations when we would benefit from pretty-printing expressions. The only situation where this kind of pretty printing would be really beneficial are errors obtained when two values cannot be lubed because the slicing criterion has different structure than result of computations. But putting resugaring there requires some very careful thinking due to mentioned partiality of resugaring. It would be very confusing if trying to display an error message lead to resugaring error being produced.