[Grace-core] Gradual Typing for Generics

[Kim Bruce]

Makes sense to me.  I would like to see compiler/interpreter flags that allow the programmer a choice of which route to take -- stop programs that are provably erroneous from running vs let them run and get the counterexample (strict vs permissive).  Ideally, whichever flag was chosen, the programmer would get a message explaining why it was provably erroneous to help guide them in fixing the problem.

In my experience some people do better with a logical explanation of why there is an error and others do better with seeing the program actually crash with fixed values.  If we allow them to flip back and forth with minimal effort, it should be helpful to everyone.  I would probably choose the strict flag for the initial run and if I couldn't understand the problem, I would go for the counterexample.  I suspect Andrew would do the reverse.

Note by the way that if no types are provided (everything is dynamic) then the system would be unlikely to raise anything like a type error.

Kim



On Sep 16, 2011, at 8:52 AM, Andrew P. Black wrote:

> 
> On 15 Sep 2011, at 18:04, Kim Bruce wrote:
> 
>> On Sep 15, 2011, at 4:59 PM, Andrew P. Black wrote:
>> 
>>> 
>>> If the type-checker can guarantee that a run-time type check will always fail, it's good to allow the programmer to be warned of this problem.  It's also good to allow the programmer to run the program anyway, and examine the dynamic error that is produced.  This error will provide a counterexample, and may make it a lot clearer why the program is wrong than any statically-produced textual error message
>> 
>> I think this is an implementation issue, but certainly sounds reasonable.  I believe Eclipse often asks if you want to try to run a program even if it has static errors (though most of the time that seems to fail when it actually attempts it).
>> 
>> Kim
> 
> I agree that It's an implementation issue _second_, but before that it's a semantic issue.  Is a program with a type error a program, or a non-program?  If we agree it's a program, and give it a semantics (like "Message-not-understood"), then it's possible for the implementation to run it (and, hopefully, produce  "MNU" as the answer!)  However, if we say that it's a non-program, then the implementation can't run it.
> 
> 	Andrew
>