[Grace-core] On Gradual Typing

[James Noble]

> Regarding compiler modes, I would distinguish gradual typing from
> "just ignore the errors".

absolutely.  
Think about C# and (now) Scala with an *explicit* type Dynamic:
these can be considered gradually typed - but not "optionally" typed.

Then typing for things like Grace (or Dart) is basically in the same
class as these systems except that some/all omitted types are 
treated as dynamic implicitly - and others may be inferred
(as in defs, and blocks?) 

I think for defs, it may not matter if they are taken to be dynamic
or inferred somehow, as no extra *runtime* errors will be caused.
That's not true for vars, say, not sure about blocks/lambdas...

> The idea is that a gradual typer knows
> *which* errors to emit. It knows *which* errors a programmer really
> ought to care about. When working with a gradual-typing compiler, the
> norm is still that you respond to all error messages.

right.  Although there are some errors that really prevent execution -
parse errors, for example.  Although, again, there is more we could do:
e.g. only stop running when we arrive at a syntactically incorrect method,
rather than anytime we find a syntactically incorrect program. 

I've no idea how to express these distinctions in the specification.

Perhaps there are "fatal" and "non-fatal" compile time / static errors.
The distinction is based on pragmatics of any implementation.
Dialect checkers may raise errors or warnings - but implementations
should still run programs with such errors or warnings. 
Finally there are a many things that should be run-time errors - 
type errors, mostly, I'd guess. 

So then, arguably the question on abstract/complete is: 
which category should that be?  Something so important
that it really should be fatal, should stop programs, or not? 
Dart put "concrete" into the language, but I'm still not convinced
it needs to be.  Their rationale is:

> We want different behavior for concrete classes and abstract classes. If A is intended to be abstract, we want the static checker to warn about any attempt to instantiate A, and we do not want the checker to complain about unimplemented methods in A. In contrast, if A is intended to be concrete, the checker should warn about all unimplemented methods, but allow clients to instantiate it freely

from http://www.dartlang.org/docs/spec/latest/dart-language-specification.html#h.ed5f44k6gfp
 


Note that Dart goes further and - by running in "production mode" - would not 
raise type check errors even in code like this:

def s : Sting
s := 3 

until - somewhere - s receives a request that 3 doesn't understand. 
We're *not* suggesting any such semantics for Grace.  Even under the most 
liberal interpretation, this code should raise a runtime error at the assignment.

I think Andrews three options all fit in here:
>  - Under the Bush interpretation, all checks will be performed at runtime.

    (kjx) all except fatal errors that mean there's nothing to run.
>  - Under the Murrow interpretation, you will get a mix of compile-time warnings and run-time check
    (kjx) fatal errors stop you running. "typechecker" / "dialects" give warnings
>  - Under the Wilson interpretation, you won't be permitted to run a program that might have a type-error

    (kjx) fatal errors stop you running. "typechecker" / "dialects" also stop you running

James.