[Grace-core] On Gradual Typing

[Andrew P Black]

On 18 Jul 2013, at 15:31 , Michael Homer wrote:

> The point is that you don't know what inherits from it (statically,
> probably), and so with a static typechecker it is an error. It isn't
> necessarily wrong dynamically, and if the typechecker is fully
> disabled by an out-of-band lever then the program should be fine.

I had assumed that the point of a type-checker was to help me find errors, not to stop me writing an abstract superclass.

>> I want an IDE that will remind me that the above object requires a y method.  I don't want an IDE that will prevent me from running tests on a program that contains such an object.
> Yes you do. That is why I wrote these examples.

No, really. I don't.   There has to be, at the very least, an annotation that will say: "yes, I know that a method y must be supplied before this is used."  Press on!

>> Why would the type-checker need to modify the behaviour of the program?  Can you give an example?
> Anywhere that you infer a generic parameter. It is an actual concrete
> argument to the method.

So, in your iterator example, are you saying that the staically-typed version of for()do() actually needs an additional run-time argument? 
In other words, that the method is really for<>()do()?  What does the method do with this argument at runtime?

I had been assuming that the stuff in the < and > brackets were parameterized annotations, and existed for the benefit of the checker.

I can see that if you are doing an explicit run-time type check, as with a request of match, then you will need the type at run time.  But in this case it will need to be a real argument, passed into the method regardless of whether or not there is static type-checking.

	Andrew