[Grace-core] On Gradual Typing

[Andrew P Black]

Thanks for opening this dissuasion, Michael.


On 17 Jul 2013, at 02:56 , Michael Homer wrote:

> So far, the conception of how gradual typing works in Grace has been
> that the typechecker is always there, but that by using "Dynamic" or
> omitting the annotations you can get dynamically typed code that the
> typechecker doesn't do anything with.

That wasn't how it we imagine it at least at some time in the past — we imagined a lever on the side of the IDE that told it how to 
respond to type errors.

> The type annotations do not have any effect on the run-time
> behaviour,

Sure they do.  Exactly _what_ effect is open, though.   If I add the annotation ": X" to the declaration of var v, I might expect one or all of the following:

	(1) That any assignment to v of an object that is not an X will produce a runtime error
	(2) That any assignment to v of an object that cannot be statically proven to be an X will produce a static error.
	(3) That any request of a method on v that is not in X is a static error
	(4) That any request of a method on v that is not in X is a dynamic error, regardless of whether the object bound to v actually understands X

We can pick a subset of these effects, or we can make it depend on the position of the lever.   Of course, it would be better to make the semantics of the language independent of the position of such a lever, but that would require agreeing on the right subset!

Michael, what is your first problem?   Some code requests y on self, and the compiler is able to prove that self don't (yet) have a y.   What's the issue?  Whether the system should issue a warning?  Whether it should let the student run the program?   Or what?   

> Is there even a "Block" type? The type of
> 1    { v : Number -> print(v) }
> seems like it must be roughly { apply(_ : Number) -> Done }. What about
> 2    { print "OK" }
> ? It must be { apply() -> Done }, while
> 3    { a : Number, b : Number -> print(a + b) }
> must be { apply(_ : Number, _ : Number) -> Done }. The common
> supertype of these types is {}, the top type, because the methods have
> different parameter counts.

This is exactly why we allowed overloading by NUMBER of arguments in Emerald.  It means that the common supertype of all of these has 3 apply methods, with zero, one and two arguments.    I don't understand why Grace doesn't do the same.  

The alternative would be to make apply a varargs method, which I think means that checking that an application of a function has been given the correct number of arguments must be postponed until runtime.

	Andrew