[Grace-core] On Gradual Typing

[Michael Homer]

On Fri, Jul 19, 2013 at 10:47 AM, Andrew P Black
<andrew.p.black at gmail.com> wrote:
>
> 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.
All sensible static typecheckers I can think of will give an error
here; it is certainly what Kim wants to happen. If you're not using
the typechecker then obviously you can do whatever you want, but if
you are then it is almost certainly an error.
>>> 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!
Sorry, that was ambiguous. I meant yes, you do want that, which was
why I wrote them. The point of the examples was to highlight where the
different goals came into conflict, and how I think from how (at least
how I think) the current language definition goes, you can't actually
write fully dynamic code. James has come in to say that yes, you can;
Kim has come in to say you shouldn't be able to; and obviously you
want to write exactly this code. Now you all get to argue it out.
>>> 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.
The language has been stipulated to have retained generics, so yes, it
is a real argument, and yes, it is written differently than the
others. Obviously that can be changed too, but it is the status quo.
-Michael