[Ur] typechecker rejects form handler

[Jason Gross]

I agree that unnecessarily chatty error messages are bad, though, from what
little I've seen, I think the existing error messages are sometimes already
too chatty.  For example, I suspect that this error message would be easier
to read if it said something like:

In environment
?292::{?U}
?293::{?V}
?294::Type

Expression:  s.#Text
  Have con:  string
  Need con:  [?292 ~ ?293] => ?294

Incompatible constructors
Have:  string
Need:  [?292 ~ ?293] => ?294

In general, I think it's better to have more lines with a lower information
density; that way, I can pick how much I want to consider at once, and
don't need to think about the types of unification variables if the shape
is already wrong.

I also think that in the case where it's not immediately obvious what the
fix is from the type mismatch, it can be helpful to know where the
constraints come from (possibly this information should be conditionally
enabled with a verbosity flag).  For example,

...

Expression:  s.#Text
  Have con:  string
    From filename:linenumber:range:
    fun validator (s:{Text:string}) : transaction page =
                           ~~~~~~~
  Need con:  [?292 ~ ?293] => ?294
    From filename:linenumber:range
     case s.Text !  = "" of
             ~~~~~

Incompatible constructors
Have:  string
Need:  [?292 ~ ?293] => ?294

or something like that, and perhaps have an "even more verbose" option that
gives the type of the head of the enclosing expression, as well as all of
its arguments and their types?

I seem to recall finding the error messages rather impenetrable when I
tried to learn Ur/Web, and they're part of the reason I still haven't
gotten around to learning it (the others are: not as many examples around
as, e.g., python, javascript, Coq; lack of time).

-Jason



On Sun, Jan 5, 2014 at 1:15 PM, Adam Chlipala <adamc at csail.mit.edu> wrote:

> On 01/04/2014 02:43 PM, Jason Gross wrote:
>
>> As an idea to improve error messages, would it be possible to tag
>> unification hints with where they come from, so that the error message
>> would include something like "... constraint comes from passing 's.Text' as
>> an argument to postfix '!'" or something?
>>
>
> That's an interesting idea.  My first reaction is that the extra
> information you're suggesting is easy to deduce by inspecting the code.  A
> unification failure for an expression is only triggered in the context of
> its immediately enclosing parent expression.
>
> However, I'd never before considered the consequences of parsing
> misunderstandings like this one!  Effectively, shouting out the kind of
> enclosing parent expression could help the user see how the code is really
> being parsed.
>
> At the same time, chattier type inference output can make messages harder
> to read in the common case, and I've never seen this particular kind of
> error come up in the wild before.  So, for now, I think I'll leave the
> error messages alone, but I'll keep your suggestion in mind.
>
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20140105/191d6f91/attachment.html>